Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2000-09-20 15:30:03 -0700 (Wed, 20 Sep 2000)
Revision: 3067
Log message:

      1) Added a new theory (itt_disect) about dependent intersection.
      
      2) Fixed rules intersectionElimination and intersectionSubtype in itt_isect
      
      3) Added a correct version of  intersectionMemberFormation
      
      4) Fixed some comments
      
      5) Added a new bug (4.10) in BUGS
      

Changes  Path
+7 -0 metaprl/BUGS
+1 -0 metaprl/doc/latex/theories/itt/print.ml
+1 -0 metaprl/theories/itt/Makefile
Added metaprl/theories/itt/itt_disect.ml
Properties metaprl/theories/itt/itt_disect.ml
Added metaprl/theories/itt/itt_disect.mli
Properties metaprl/theories/itt/itt_disect.mli
+15 -4 metaprl/theories/itt/itt_isect.ml
+13 -3 metaprl/theories/itt/itt_isect.mli
+1 -1 metaprl/theories/itt/itt_prod.mli
+2 -1 metaprl/theories/itt/itt_tunion.ml