Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-17 18:02:23 -0700 (Sun, 17 Oct 2004)
Revision: 6244
Log message:

      1. Addressing the bug 322 (first part about nat)
      2. Rationals are normalized pairs of integers now (gcd=1)
      3. Rational polynomial normalization
      ToDo: Grounding intermediate assertion of SupInf.
      Doing this efficently is somewhat challenging.
      

Changes  Path
+1 -2 metaprl/theories/itt/OMakefile
+46 -9 metaprl/theories/itt/itt_int_arith.ml
+5 -4 metaprl/theories/itt/itt_int_arith.mli
+5 -1 metaprl/theories/itt/itt_nat.ml
+1450 -1392 metaprl/theories/itt/itt_nat.prla
+266 -38 metaprl/theories/itt/itt_rat.ml
+23 -12 metaprl/theories/itt/itt_rat.mli
+9526 -5392 metaprl/theories/itt/itt_rat.prla
+48 -10 metaprl/theories/itt/itt_rat2.ml
+5049 -3207 metaprl/theories/itt/itt_rat2.prla
+215 -108 metaprl/theories/itt/itt_supinf.ml
+1 -0 metaprl/theories/itt/itt_supinf.mli