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
|
\DOC FIRST
\TYPE {FIRST : tactic list -> tactic}
\SYNOPSIS
Applies the first tactic in a tactic list that succeeds.
\KEYWORDS
tactical.
\DESCRIBE
When applied to a list of tactics {[t1;...;tn]}, and a goal {g}, the tactical
{FIRST} tries applying the tactics to the goal until one succeeds. If the
first tactic which succeeds is {tm}, then the effect is the same as just {tm}.
Thus {FIRST} effectively behaves as follows:
{
FIRST [t1;...;tn] = t1 ORELSE ... ORELSE tn
}
\FAILURE
The application of {FIRST} to a tactic list never fails. The resulting
tactic fails iff all the component tactics do when applied to the goal,
or if the tactic list is empty.
\SEEALSO
EVERY, ORELSE.
\ENDDOC
|
