1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
\DOC ORELSE_TCL
\TYPE {(ORELSE_TCL) : thm_tactical -> thm_tactical -> thm_tactical}
\SYNOPSIS
Applies a theorem-tactical, and if it fails, tries a second.
\KEYWORDS
theorem-tactical.
\DESCRIBE
When applied to two theorem-tacticals, {ttl1} and {ttl2}, a theorem-tactic
{ttac}, and a theorem {th}, if {ttl1 ttac th} succeeds, that gives the
result. If it fails, the result is {ttl2 ttac th}, which may itself fail.
\FAILURE
{ORELSE_TCL} fails if both the theorem-tacticals fail when applied to the
given theorem-tactic and theorem.
\SEEALSO
EVERY_TCL, FIRST_TCL, THEN_TCL.
\ENDDOC
|
