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
|
\DOC EVERY
\TYPE {EVERY : tactic list -> tactic}
\SYNOPSIS
Sequentially applies all the tactics in a given list of tactics.
\KEYWORDS
tactical.
\DESCRIBE
When applied to a list of tactics {[t1; ... ;tn]}, and a goal {g}, the tactical
{EVERY} applies each tactic in sequence to every
subgoal generated by the previous one. This can be represented as:
{
EVERY [t1;...;tn] = t1 THEN ... THEN tn
}
\noindent If the tactic list is empty, the resulting tactic has no effect.
\FAILURE
The application of {EVERY} to a tactic list never fails. The resulting
tactic fails iff any of the component tactics do.
\COMMENTS
It is possible to use {EVERY} instead of {THEN}, but probably
stylistically inferior. {EVERY} is more useful when applied to a list of
tactics generated by a function.
\SEEALSO
FIRST, MAP_EVERY, THEN.
\ENDDOC
|
