Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-03 20:53:07 -0800 (Fri, 03 Dec 2004)
Revision: 6320
Log message:

      Now SupInf handles trivially contradictory inequalities correctly (like 0>5)
      and quickly, before it was completely missing them because of the design.
      In particular, it now proofs inttestn/1.
      

Changes	Path
+0 -8	metaprl/refiner/reflib/supinf.ml
+0 -4	metaprl/refiner/reflib/supinf.mli
+120 -431	metaprl/theories/itt/itt_supinf.ml
+2 -2	metaprl/theories/itt/itt_supinf.mli