Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-07 03:23:21 -0700 (Wed, 07 May 2003)
Revision: 4573
Log message:
- Added the fall-back for dT's elim. Now if several rules/tactics are added
to elim resource for the same term, dT will try them all until one succeeds
instead of only trying the first one. Note that dT 0 (intro) was doing this
for a very long time.
- Added nil sequents args to sequents in comments on support/tactics modules
(forgot this in my previous commit).
- Added another version of elimination rule for quotients, as Xin requested.