UNDISCH_TAC : term -> tactic
STRUCTURE
Tactic
SYNOPSIS
Undischarges an assumption and deletes all assumptions that are alpha-equivalent to it.
DESCRIPTION
Let a1 to an be the assumptions that are alpha-equivalent to v, then 
               A ?- t
   ==============================  UNDISCH_TAC v
    A - {a1, ..., an} ?- v ==> t

In particular, if v is among the assumptions of the goal and no other assumption is alpha-equivalent to it, then UNDISCH_TAC behaves as the opposite of DISCH_TAC: 

          A ?- t
   ====================  UNDISCH_TAC v
    A - {v} ?- v ==> t
FAILURE
UNDISCH_TAC fails if no assumption is alpha-equivalent to v.
COMMENTS
In the typical use v is among the assumptions. If only a single assumption alpha-equivalent to v, but it is different from v then the action of UNDISCH_TAC can be seen as undischarging followed by alpha-conversion.
SEEALSO
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, NEG_DISCH, FILTER_DISCH_TAC, FILTER_DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_ALL
HOL  Kananaskis-13