Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-09 22:52:49 -0800 (Tue, 09 Nov 2004)
Revision: 6257
Log message:

      New code that generates trace of supinf's reasoning and than constructs the proof.
      It proves all but the biggest test (itt_supinf/inttestn).
      Couldn't submit the proofs because metaprl crashes on export.
      

Changes  Path
+298 -89 metaprl/refiner/reflib/supinf.ml
+71 -7 metaprl/refiner/reflib/supinf.mli
+23 -13 metaprl/theories/itt/itt_rat.ml
+2 -0 metaprl/theories/itt/itt_rat.mli
+7 -3 metaprl/theories/itt/itt_rat2.ml
+0 -0 metaprl/theories/itt/itt_rat2.mli
+519 -88 metaprl/theories/itt/itt_supinf.ml
+10 -0 metaprl/theories/itt/itt_supinf.mli