Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-16 21:28:25 -0800 (Tue, 16 Dec 2003)
Revision: 5184
Log message:

      Merging new-then_Lab_T-implementation branch to main trunk.
      thenMLT and alike still not supported.
      

Changes  Path
+2 -0 metaprl/refiner/refsig/thread_refiner_sig.ml
+3 -0 metaprl/tactics/null/thread_refiner.ml
+15 -0 metaprl/tactics/proof/tactic_boot.ml
+2 -0 metaprl/tactics/proof/tactic_boot_sig.ml
+7 -20 metaprl/tactics/proof/tacticals_boot.ml