Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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.