UNDISCH_TM
Drule.UNDISCH_TM : thm -> term * thm
Undischarges the antecedent of an implicative theorem, also returning that antecedent.
A |- t1 ==> t2
---------------- UNDISCH_TM
A, t1 |- t2
Note that UNDISCH_TM treats "~u" as "u ==> F".
Failure
UNDISCH_TM will fail on theorems which are not implications or
negations.
Comments
If the antecedent already appears in (or is alpha-equivalent to one of) the hypotheses, it will not be duplicated.
UNDISCH_TM is similar to UNDISCH except that it also returns the
antecedent concerned, which may be useful, for example, when the new
assumption is subsequently to be discharged