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
|
\DOC USE_THEN
\TYPE {USE_THEN : string -> thm_tactic -> tactic}
\SYNOPSIS
Apply a theorem tactic to named assumption.
\DESCRIBE
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
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.
\SEEALSO
ASSUME, FIND_ASSUM, HYP, LABEL_TAC, REMOVE_THEN.
\ENDDOC
|
