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
|
\DOC REPEAT
\TYPE {REPEAT : tactic -> tactic}
\SYNOPSIS
Repeatedly applies a tactic until it fails.
\KEYWORDS
tactical.
\DESCRIBE
The tactic {REPEAT t} is a tactic which applies {t} to a goal, and while it
succeeds, continues applying it to all subgoals generated.
\FAILURE
The application of {REPEAT} to a tactic never fails, and neither does the
composite tactic, even if the basic tactic fails immediately, unless it raises
an exception other that {Failure ...}.
\EXAMPLE
If we start with a goal having many universal quantifiers:
{
# g `!w x y z. w < z /\ x < y ==> w * x + 1 <= y * z`;;
}
\noindent then {GEN_TAC} will strip them off one at a time:
{
# e GEN_TAC;;
val it : goalstack = 1 subgoal (1 total)
`!x y z. w < z /\ x < y ==> w * x + 1 <= y * z`
}
\noindent and {REPEAT GEN_TAC} will strip them off as far as possible:
{
# e(REPEAT GEN_TAC);;
val it : goalstack = 1 subgoal (1 total)
`w < z /\ x < y ==> w * x + 1 <= y * z`
}
Similarly, {REPEAT COND_CASES_TAC} will eliminate all free conditionals in the
goal instead of just one.
\SEEALSO
EVERY, FIRST, ORELSE, THEN, THENL.
\ENDDOC
|
