Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-09 19:32:09 -0700 (Wed, 09 Jul 2008)
Revision: 13105
Log message:

      Changed the families handling code because merging of families was incorrectly implemented. It used to be amp from representatives to the whole family, but if you think even a bit, you'll realize that it can't work. Now it's a set (list) of sets (families), not very efficient but can be replaced with an ordered set with a natural(lexicographical) order on families.
     
     We forgot to replace every provisional from a principal family with the summ of all essential terms - we did it only for BoxRight rule, have to do it uniformly.

Changes  Path(relative to metaprl/theories/s4lp)
+277 -78 hilbert_internal.ml