1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
\DOC REMOVE_THEN
\TYPE {REMOVE_THEN : string -> thm_tactic -> tactic}
\SYNOPSIS
Apply a theorem tactic to named assumption, removing the assumption.
\DESCRIBE
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
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.
\SEEALSO
ASSUME, FIND_ASSUM, HYP, LABEL_TAC, USE_THEN.
\ENDDOC
|
