Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-14 04:38:34 -0700 (Wed, 14 May 2003)
Revision: 4597
Log message:
Changed the genAssumT tactic to put things into hypothesis list.
More specifically, all assumtions up to the first membership one
(inclusively) will be turned into hypothesis, and only the ones after
the first membership one will go into conclusion using the universal
quanitifier and implication, as before.
The main reason for this change is that the manual "dT 0" would generate
wf subgoals that are trivially true, but could require non-trivial amount
of typing.