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
28
29
30
31
32
33
34
35
|
\DOC THEN
\TYPE {$THEN : (tactic -> tactic -> tactic)}
\SYNOPSIS
Applies two tactics in sequence.
\KEYWORDS
tactical.
\DESCRIBE
If {T1} and {T2} are tactics, {T1 THEN T2} is a tactic which applies {T1} to a
goal, then applies the tactic {T2} to all the subgoals generated. If {T1}
solves the goal then {T2} is never applied.
\FAILURE
The application of {THEN} to a pair of tactics never fails.
The resulting tactic fails if {T1} fails when applied to the goal, or if
{T2} does when applied to any of the resulting subgoals.
\COMMENTS
Although normally used to sequence tactics which generate a single subgoal,
it is worth remembering that it is sometimes useful to apply the same tactic
to multiple subgoals; sequences like the following:
{
EQ_TAC THENL [ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]]
}
\noindent can be replaced by the briefer:
{
EQ_TAC THEN ASM_REWRITE_TAC[]
}
\SEEALSO
EVERY, ORELSE, THENL.
\ENDDOC
|
