Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-02-22 19:29:08 -0800 (Sat, 22 Feb 2003)
Revision: 4111
Log message:
- Added more automation to itt_int_base and itt_int_ext
(reductions for "a - b + b", "a + b - b", "a - a", "a < a", etc)
- Simplified the Itt_nat proofs using the new automation
(most of the proofs are still incomplete since they need an inequality
tactic).