Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-06-17 14:41:29 -0700 (Sun, 17 Jun 2001)
Revision: 3274
Log message:

      - Added tacticals whileProgressMT and untilFailMT
      
      - Implemented dependend records
      
      - Change a rule for depended intersection
      

Changes  Path
+4 -2 metaprl/doc/itt_quickref.txt
+2 -0 metaprl/filter/boot/tactic_boot_sig.mlz
+5 -0 metaprl/filter/boot/tacticals_boot.ml
+20 -6 metaprl/theories/itt/itt_disect.ml
+210 -99 metaprl/theories/itt/itt_record.ml
+15 -7 metaprl/theories/itt/itt_record.mli
+6 -7 metaprl/theories/itt/itt_record0.ml
+23 -23 metaprl/theories/itt/itt_record_exm.ml
+26 -24 metaprl/theories/itt/itt_record_label.ml
+2 -2 metaprl/theories/itt/itt_record_label.mli
+18 -0 metaprl/theories/tactic/perv.ml
+7 -4 metaprl/theories/tactic/top_tacticals.ml
+2 -0 metaprl/theories/tactic/top_tacticals.mli