REMOVE_THEN : string -> thm_tactic -> tactic
- SYNOPSIS
-
Apply a theorem tactic to named assumption, removing the assumption.
- DESCRIPTION
-
The tactic REMOVE_THEN "name" ttac applies the theorem-tactic ttac to the
assumption labelled name (or the first in the list if there is more than
one), removing the assumption from the goal.
- FAILURE CONDITIONS
-
Fails if there is no assumption of that name or if the theorem-tactic fails
when applied to it.
- EXAMPLE
-
See LABEL_TAC for a relevant example.
- USES
-
Using an assumption identified by name that will not be needed again in the
proof.
- SEE ALSO
-
ASSUME, FIND_ASSUM, HYP, LABEL_TAC, USE_THEN.