UNDISCH_TAC : term -> tactic
STRUCTURE
Tactic
SYNOPSIS
Undischarges an assumption.
DESCRIPTION
          A ?- t
   ====================  UNDISCH_TAC v
    A - {v} ?- v ==> t

FAILURE
UNDISCH_TAC will fail if "v" is not an assumption.
COMMENTS
UNDISCHarging v will remove all assumptions which are identical to v, but those which are alpha-equivalent will remain.
SEEALSO
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, NEG_DISCH, FILTER_DISCH_TAC, FILTER_DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_ALL
HOL  Kananaskis-10