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
|
\DOC EVERY_TCL
\TYPE {EVERY_TCL : (thm_tactical list -> thm_tactical)}
\SYNOPSIS
Composes a list of theorem-tacticals.
\KEYWORDS
theorem-tactical.
\DESCRIBE
When given a list of theorem-tacticals and a theorem, {EVERY_TCL} simply
composes their effects on the theorem. The effect is:
{
EVERY_TCL [ttl1;...;ttln] = ttl1 THEN_TCL ... THEN_TCL ttln
}
\noindent In other words, if:
{
ttl1 ttac th1 = ttac th2 ... ttln ttac thn = ttac thn'
}
\noindent then:
{
EVERY_TCL [ttl1;...;ttln] ttac th1 = ttac thn'
}
\noindent If the theorem-tactical list is empty, the resulting theorem-tactical
behaves in the same way as {ALL_THEN}, the identity theorem-tactical.
\FAILURE
The application to a list of theorem-tacticals never fails.
\SEEALSO
FIRST_TCL, ORELSE_TCL, REPEAT_TCL, THEN_TCL.
\ENDDOC
|
