Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2001-11-15 12:25:28 -0800 (Thu, 15 Nov 2001)
Revision: 3442
Log message:

      Itt_int_ext: more conversions added to reduce resource
      
      Itt_int_arih: first working version of arithT!!!
      You can observe proof of test rule and try to replace it with just arithT
      in the root.
      While now arithT knows only numbers, variables and +
      

Changes	Path
+29 -7	metaprl/theories/itt/itt_int_arith.ml
+7 -1	metaprl/theories/itt/itt_int_arith.mli
+6 -0	metaprl/theories/itt/itt_int_ext.ml
+0 -0	metaprl/theories/itt/itt_int_ext.mli