Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-05-05 20:13:51 -0700 (Mon, 05 May 2003)
Revision: 4564
Log message:

      1.The proof of itt_nat/positive_rule1 is fixed.
      2.One more bug/unaccounted case fixed in arithT.
      

Changes  Path
+2 -2 metaprl/theories/itt/itt_int_arith.ml
+7 -0 metaprl/theories/itt/itt_int_arith.mli
+1286 -1976 metaprl/theories/itt/itt_nat.prla