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.