Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 05:43:00 -0800 (Mon, 26 Jan 2004)
Revision: 5281
Log message:

      Some progress towards proper definitions for itt_poly operations. Some proofs
      are still incomplete - we need a stronger indEqual (see my post in the newsgroup)
      to finish those proofs.
      

Changes  Path
+1 -1 metaprl/theories/itt/itt_logic.ml
+6 -0 metaprl/theories/itt/itt_nat.ml
+1635 -818 metaprl/theories/itt/itt_nat.prla
+9 -29 metaprl/theories/itt/itt_poly.ml
+2 -6 metaprl/theories/itt/itt_poly.mli
+2455 -4984 metaprl/theories/itt/itt_poly.prla