Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-18 22:57:51 -0700 (Tue, 18 May 2004)
Revision: 5792
Log message:

      makefiles - removed references to itt_mpoly
      itt_mpoly2 - switched to W-type (up to this didn't use any recursion-type),
      AFAI understand W-type permits to do structural induction;
      proved several lemmas
      

Changes	Path
+0 -1	metaprl/theories/itt/Makefile
+0 -1	metaprl/theories/itt/OMakefile
+51 -9	metaprl/theories/itt/itt_mpoly2.ml
+6702 -6297	metaprl/theories/itt/itt_mpoly2.prla