Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-06 16:13:39 -0800 (Fri, 06 Feb 2004)
Revision: 5343
Log message:

      1.arith - Aleksey's suggestions implemented but not really used yet.
      2.supinf - some theory-independent parts moved outside.
      3.term_order - comparison of terms moved outside of itt_int_arith,
      comparison of bound-terms implemented in correct way (hopefully).
      

Changes  Path
+3 -1 metaprl/refiner/reflib/Files
+73 -30 metaprl/refiner/reflib/arith.ml
+5 -2 metaprl/refiner/reflib/arith.mli
Added metaprl/refiner/reflib/supinf.ml
Properties metaprl/refiner/reflib/supinf.ml
Added metaprl/refiner/reflib/supinf.mli
Properties metaprl/refiner/reflib/supinf.mli
Added metaprl/refiner/reflib/term_order.ml
Properties metaprl/refiner/reflib/term_order.ml
Added metaprl/refiner/reflib/term_order.mli
Properties metaprl/refiner/reflib/term_order.mli
+56 -111 metaprl/theories/itt/itt_int_arith.ml
+38 -257 metaprl/theories/itt/itt_supinf.ml