USE_THEN : string -> thm_tactic -> tactic

SYNOPSIS: Apply a theorem tactic to named assumption.
DESCRIPTION: The tactic USE_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).
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 an extended example.
USES: Using an assumption identified by name.
SEE ALSO: ASSUME, FIND_ASSUM, HYP, LABEL_TAC, REMOVE_THEN.