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
|
\DOC FIRST_TCL
\TYPE {FIRST_TCL : thm_tactical list -> thm_tactical}
\SYNOPSIS
Applies the first theorem-tactical in a list that succeeds.
\KEYWORDS
theorem-tactical.
\DESCRIBE
When applied to a list of theorem-tacticals, a theorem-tactic and a theorem,
{FIRST_TCL} returns the tactic resulting from the application of the first
theorem-tactical to the theorem-tactic and theorem that succeeds. The effect
is the same as:
{
FIRST_TCL [ttl1;...;ttln] = ttl1 ORELSE_TCL ... ORELSE_TCL ttln
}
\FAILURE
{FIRST_TCL} fails iff each tactic in the list fails when applied to the
theorem-tactic and theorem. This is trivially the case if the list is empty.
\SEEALSO
EVERY_TCL, ORELSE_TCL, REPEAT_TCL, THEN_TCL.
\ENDDOC
|
