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 ALL_THEN
\TYPE {ALL_THEN : thm_tactical}
\SYNOPSIS
Passes a theorem unchanged to a theorem-tactic.
\KEYWORDS
theorem-tactic, identity.
\DESCRIBE
For any theorem-tactic {ttac} and theorem {th}, the application {ALL_THEN ttac
th} results simply in {ttac th}, that is, the theorem is passed unchanged to
the theorem-tactic. {ALL_THEN} is the identity theorem-tactical.
\FAILURE
The application of {ALL_THEN} to a theorem-tactic never fails. The resulting
theorem-tactic fails under exactly the same conditions as the original one
\USES
Writing compound tactics or tacticals, e.g. terminating list iterations
of theorem-tacticals.
\SEEALSO
ALL_TAC, FAIL_TAC, NO_TAC, NO_THEN, THEN_TCL, ORELSE_TCL.
\ENDDOC
|
