UNDISCH_THEN : term -> thm_tactic -> tactic
- SYNOPSIS
-
Undischarges an assumption and applies theorem-tactic to it.
- DESCRIPTION
-
The tactic UNDISCH_THEN `a` ttac applied to a goal A |- t takes a out of
the assumptions to give a goal A - {a} |- t, and applies the theorem-tactic
ttac to the assumption .. |- a and that new goal.
- FAILURE CONDITIONS
-
Fails if a is not an assumption; when applied to the goal it fails exactly if
the theorem-tactic fails on the modified goal.
- COMMENTS
-
The tactic UNDISCH_TAC `t` can be considered the special case of
UNDISCH_THEN `t` MP_TAC.
- SEE ALSO
-
FIND_ASSUM, FIRST_X_ASSUM, UNDISCH_TAC.