Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-13 21:28:07 -0700 (Sun, 13 Aug 2000)
Revision: 3047
Log message:

      I changed the unhide rules according to hide{A} = squash{A} semantics.
      
      Alexei, can you take a look at my changes and see if you agree with them?
      Also, do we need more elimination rules for union and more introduction rules
      for intersection?
      

Changes  Path
+3 -9 metaprl/BUGS
+0 -4 metaprl/theories/itt/itt_bool.ml
+4437 -4817 metaprl/theories/itt/itt_bool.prla
+4 -4 metaprl/theories/itt/itt_bunion.ml
+227 -193 metaprl/theories/itt/itt_bunion.prla
+91 -91 metaprl/theories/itt/itt_esquash.prla
+8 -5 metaprl/theories/itt/itt_isect.ml
+0 -10 metaprl/theories/itt/itt_isect.mli
+1182 -1222 metaprl/theories/itt/itt_isect.prla
+4 -3 metaprl/theories/itt/itt_set.ml
+7 -4 metaprl/theories/itt/itt_tunion.ml
+3 -3 metaprl/theories/itt/itt_tunion.mli