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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
\DOC ORELSE
\TYPE {(ORELSE) : tactic -> tactic -> tactic}
\SYNOPSIS
Applies first tactic, and iff it fails, applies the second instead.
\KEYWORDS
tactical.
\DESCRIBE
If {t1} and {t2} are tactics, {t1 ORELSE t2} is a tactic which applies {t1} to
a goal, and iff it fails, applies {t2} to the goal instead.
\FAILURE
The application of {ORELSE} to a pair of tactics never fails.
The resulting tactic fails if both {t1} and {t2} fail when applied to the
relevant goal.
\EXAMPLE
The tactic {STRIP_TAC} breaks down the logical structure of a goal in various
ways, e.g. stripping off universal quantifiers and putting the antecedent of
implicational conclusions into the assumptions. However it does not break down
equivalences into two implications, as {EQ_TAC} does. So you might start
breaking down a goal corresponding to the inbuilt theorem {MOD_EQ_0}
{
# g `!m n. ~(n = 0) ==> ((m MOD n = 0) <=> (?q. m = q * n))`;;
...
}
\noindent as follows
{
# e(REPEAT(STRIP_TAC ORELSE EQ_TAC));;
val it : goalstack = 2 subgoals (2 total)
0 [`~(n = 0)`]
1 [`m = q * n`]
`m MOD n = 0`
0 [`~(n = 0)`]
1 [`m MOD n = 0`]
`?q. m = q * n`
}
\SEEALSO
EVERY, FIRST, THEN.
\ENDDOC
|
