Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-11 22:11:21 -0800 (Thu, 11 Dec 2003)
Revision: 5174
Log message:

      1. wrap_terms added to null-refiner for postprocessing of tactic results
      2. implementation of "new" local semantics of thenMT, thenWT, etc moved to tactic_boot
      3. thenMLT and alike still not supported.
      
      Didn't check it with check-status. Aleksey, could you do it please?
      

Changes  Path
+2 -0 metaprl-branches/unlabeled-1.1.4/refiner/refsig/thread_refiner_sig.ml
+7 -20 metaprl-branches/unlabeled-1.2.2/tactics/proof/tacticals_boot.ml
+3 -0 metaprl-branches/unlabeled-1.2.4/tactics/null/thread_refiner.ml
+15 -0 metaprl-branches/unlabeled-1.4.2/tactics/proof/tactic_boot.ml
+2 -0 metaprl-branches/unlabeled-1.8.2/tactics/proof/tactic_boot_sig.ml