/usr/share/hol88-2.02.19940316/help/ENTRIES/REPEAT.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 | \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.
\SEEALSO
EVERY, FIRST, ORELSE, THEN, THENL.
\ENDDOC
|