Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-03-12 09:09:27 -0800 (Wed, 12 Mar 2003)
Revision: 4165
Log message:

      1. itt_bool - equivalence of "x=false in bool" and "assert(not x)".
      2. thenLocalMT, thenLocalAT, onAllLocalMHypsT added, they respect
         local labels instead of inheritted labels.
      3. itt_list2/nth_wf completed. Two issues are done manually:
      3.a. Use of (1)
      3.b. use of splitIntT for transition from "a<>b" to "a<b or a>b"
      4. several bugs fixed in arithT and normalizeC
      

Changes  Path
+10 -0 metaprl/theories/itt/itt_bool.ml
+2 -0 metaprl/theories/itt/itt_bool.mli
+1638 -820 metaprl/theories/itt/itt_bool.prla
+131 -37 metaprl/theories/itt/itt_int_arith.ml
+11 -0 metaprl/theories/itt/itt_int_arith.mli
+13862 -11976 metaprl/theories/itt/itt_int_arith.prla
+8 -1 metaprl/theories/itt/itt_int_base.ml
+4 -0 metaprl/theories/itt/itt_int_base.mli
+1916 -1556 metaprl/theories/itt/itt_int_base.prla
+17 -1 metaprl/theories/itt/itt_int_ext.ml
+4014 -3701 metaprl/theories/itt/itt_int_ext.prla
+3807 -3922 metaprl/theories/itt/itt_list2.prla