Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-05-04 01:45:12 -0700 (Fri, 04 May 2001)
Revision: 3207
Log message:

      1.Some minor changes in old files
      2.First ugly approach to Arith implementation. It just can find contradiction
        and construct contradictory inequality. Next step will be polynoms and
        inequalities normalization. It will increase range of input inequalities and
        let easily prove resulting contradictory inequality.
      

Changes  Path
Added metaprl/theories/itt/itt_int_arith.ml
Properties metaprl/theories/itt/itt_int_arith.ml
Added metaprl/theories/itt/itt_int_arith.mli
Properties metaprl/theories/itt/itt_int_arith.mli
+65 -17 metaprl/theories/itt/itt_int_base.ml
+36 -3 metaprl/theories/itt/itt_int_base.mli
+5219 -4025 metaprl/theories/itt/itt_int_base.prla
+47 -38 metaprl/theories/itt/itt_int_ext.ml
+12 -6 metaprl/theories/itt/itt_int_ext.mli
+4310 -2597 metaprl/theories/itt/itt_int_ext.prla