Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-03-29 16:52:27 -0800 (Sat, 29 Mar 2003)
Revision: 4347
Log message:

      1.Now arithT can deal with equality in conclusion (now it support lt,gt,le,ge,eq). neq is still unsupported.
      2.As much as possible of substitution reasoning is replaced with arithT in itt_nat/int_div_rem.
      
      P.S. I know that number of steps is alarmingly high, I'll look into it now.
      

Changes	Path
+9 -1	metaprl/theories/itt/itt_int_arith.ml
+15823 -13617	metaprl/theories/itt/itt_int_arith.prla
+279 -2380	metaprl/theories/itt/itt_nat.prla