UNDISCH_TAC : term -> tactic
STRUCTURE
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
HOL  Kananaskis-10