----------------------------------------------------------------------
UNDISCH_TM                                                     (Drule)
----------------------------------------------------------------------
UNDISCH_TM : thm -> term * thm

SYNOPSIS
Undischarges the antecedent of an implicative theorem,
also returning that antecedent.

KEYWORDS
rule, undischarge, antecedent.

DESCRIBE

    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
Drule.UNDISCH, Thm.DISCH.

----------------------------------------------------------------------