Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-05-10 21:52:59 -0700 (Mon, 10 May 2004)
Revision: 5765
Log message:

      next step to normalization:
      stdT field [t_1,...,t_n] T
      asserts that T is equal to T' where each t_i is replaced
      with a polynomial "x_n" evaluated on [t1...tn]
      this equality is proved automatically by (repeatT reduceT ttca)
      
      todo: lifting of polynomial evaluations in T' to outermost operation and evaluating
      it. AFAI understand it will evaluate to a "standard" form of T
      

Changes	Path
+37 -12	metaprl/theories/itt/itt_mpoly.ml
+2 -1	metaprl/theories/itt/itt_mpoly.mli
+5456 -4491	metaprl/theories/itt/itt_mpoly.prla