Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-03-29 18:51:38 -0800 (Sat, 29 Mar 2003)
Revision: 4348
Log message:

      1.Bugfix for previous commit - equality "a=b in t" in conclusion should be processed only if t is int and a is not b.
      2.Every "repeatC (sweepDnC conv)" is replaced with "repeatC (higherC conc)" they are equivalent if conv fails whenever it's not applicable (I had idC in several places). It noticably reduced number of proof steps. It also appears to be slightly faster (according to time printed by expand). It's actually strange - I expected that sweepDnC would be better - it should scan term less number of times.
      

Changes	Path
+0 -15	metaprl/Makefile
+25 -18	metaprl/theories/itt/itt_int_arith.ml