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.