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.