Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-01-27 20:43:23 -0800 (Tue, 27 Jan 2004)
Revision: 5295
Log message:

      Itt_int_ext, Itt_rat - inequalities over constants added to reduce,intro and elim resources.
      Itt_rat - some properties of >= stated.
      Itt_supinf - it can partly prove what it has to, check test2 for example,
      all remaining subgoals are massaged hyps.
      

Changes  Path
+40 -14 metaprl/theories/itt/itt_int_ext.ml
+4 -0 metaprl/theories/itt/itt_int_ext.mli
+4 -0 metaprl/theories/itt/itt_order.mli
+120 -7 metaprl/theories/itt/itt_rat.ml
+65 -0 metaprl/theories/itt/itt_rat.mli
+255 -120 metaprl/theories/itt/itt_supinf.ml
+0 -178 metaprl/theories/itt/itt_supinf.mli
+29551 -21644 metaprl/theories/itt/itt_supinf.prla