Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-31 19:13:33 -0700 (Thu, 31 Jul 2003)
Revision: 4799
Log message:
- Added an axiom thin_many that allowing thinning a whole range of hyps
at once (including thinning contexts! the new syntax makes the necessary
free variable restrictions expressible) to itt_struct and fol_struct,
deriving the original thin rule from thin_many
- Changed the thinMatchT (that is used by tactics such nthAssumT) to
use thin_many instead of thin
- Changed the Top_tacticals.prefix_thenT to check whether one of the arguments
is idT (and avoid unnecessarily nesting and copying things when it is).