Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-07 19:56:45 -0800 (Sun, 07 Dec 2003)
Revision: 5159
Log message:

      1.Major (?) change in label-dependent tacticals semantics
        (thenMT, thenAT, thenPT, thenET, onAllMHypsT, tryOnAllMHypsT.
        Now they respect local assignments of labels rather than labels inherited
        from above.
      
      2.This implementation moved from itt_int_arith.
      
      3.onAllCumulativeHypsT, onAllMCumulativeHypsT, tryOnAllCumulativeHypsT,
        tryOnAllMCumulativeHypsT added. They also consider goals added during
        their execution.
      
      4.I didn't change thenLabLT, thenMLT and thenALT because they are not used
        anywhere (as far as I can tell) and change in their semantics is not that
        straightforward. I suggest to remove them at all.
      

Changes  Path
+4 -0 metaprl/support/tactics/top_tacticals.ml
+4 -3 metaprl/support/tactics/top_tacticals.mli
+4 -0 metaprl/tactics/proof/tactic_boot_sig.ml
+84 -17 metaprl/tactics/proof/tacticals_boot.ml
+35 -92 metaprl/theories/itt/itt_int_arith.ml
+0 -5 metaprl/theories/itt/itt_int_arith.mli