Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-18 21:48:05 -0700 (Mon, 18 Aug 2003)
Revision: 4850
Log message:
- The rw*All family (rwAll, rwhAll, whAllAll, etc) will now use
allSubC to descend into the goal instead of onAllClausesT. This means that
it will now work correctly with any goal/assumption terms, not just
sequents, and that it now avoids issues with sequent contexts not being a
proper subterm.
Note that this means that the rw*All will now try to rewrite the sequent argument
as well!
- thenC, firstT, and a few other similar tacticals and conversionals now check
whether one of the argunemts is an idC (idT) and try to avoid creating
identity proof steps unnecessarily.