Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-07 02:09:27 -0800 (Fri, 07 Nov 2003)
Revision: 5078
Log message:

      1. Add tactic reduceT = rwAll reduceC.
      
      2. Clean records theories a little bit.
      

Changes  Path
+2 -0 metaprl/doc/itt_quickref.txt
+5 -1 metaprl/support/tactics/top_conversionals.ml
+1 -0 metaprl/support/tactics/top_conversionals.mli
+1 -1 metaprl/tactics/proof/conversionals_boot.ml
+2 -2 metaprl/theories/itt/itt_nequal.ml
+5 -0 metaprl/theories/itt/itt_nequal.mli
+8 -6 metaprl/theories/itt/itt_record.ml
+5 -5 metaprl/theories/itt/itt_record0.ml
+37 -10 metaprl/theories/itt/itt_record_label.ml
+1 -0 metaprl/theories/itt/itt_record_label.mli
+4 -3 metaprl/theories/itt/itt_record_label0.ml
+3 -1 metaprl/theories/itt/itt_record_label0.mli
+30 -29 metaprl/theories/itt/itt_record_renaming.ml