Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-11-21 22:39:51 -0800 (Sun, 21 Nov 2004)
Revision: 6285
Log message:
Now it does not normalize hypotheses that are not used.
Though it re-normalizes used hypotheses as many times as they used.
(will fix it next time)
At this point it is only 3.5 slower than Arith
but the speed up is mainly due inttestn which is not proved anyway.
Changes | Path |
+30 -23 | metaprl/theories/itt/itt_supinf.ml |