UNDISCH_TM : thm -> term * thm
STRUCTURE
Drule
SYNOPSIS
Undischarges the antecedent of an implicative theorem, also returning that antecedent.
DESCRIPTION
    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

SEEALSO
UNDISCH, DISCH
HOL  Kananaskis-14