Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-28 11:22:55 -0800 (Tue, 28 Dec 2004)
Revision: 6361
Log message:

      1. Omega Test added. It's not a complete implementation of the original Omega
      Test (splinters are not implemented hence it's not a complete procedure).
      In the current state it seems to be a little weaker than SupInf.
      Implementation is very straightforward, many optimizations from Pugh's paper
      are not implemented.
      
      2. All tests from itt_int_arith and itt_supinf are moved to itt_int_test
      

Changes  Path
+4 -0 metaprl/refiner/reflib/supinf.ml
+1 -0 metaprl/refiner/reflib/supinf.mli
+5 -121 metaprl/theories/itt/itt_int_arith.ml
+1 -4 metaprl/theories/itt/itt_int_arith.mli
Added metaprl/theories/itt/itt_int_test.ml
Properties metaprl/theories/itt/itt_int_test.ml
Added metaprl/theories/itt/itt_int_test.mli
Properties metaprl/theories/itt/itt_int_test.mli
Added metaprl/theories/itt/itt_int_test.prla
Properties metaprl/theories/itt/itt_int_test.prla
Added metaprl/theories/itt/itt_omega.ml
Properties metaprl/theories/itt/itt_omega.ml
Added metaprl/theories/itt/itt_omega.mli
Properties metaprl/theories/itt/itt_omega.mli
+8 -87 metaprl/theories/itt/itt_supinf.ml
+0 -14 metaprl/theories/itt/itt_supinf.mli