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