UNDISCH_TAC : term -> tactic

SYNOPSIS
Undischarges an assumption.

DESCRIPTION
          A ?- t
   ====================  UNDISCH_TAC `v`
    A - {v} ?- v ==> t

FAILURE CONDITIONS
UNDISCH_TAC will fail if `v` is not an assumption.

COMMENTS
UNDISCHarging `v` will remove all assumptions that are alpha-equivalent to `v`.

SEE ALSO
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_THEN.