/usr/share/hol88-2.02.19940316/help/ENTRIES/FIRST.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 23 24 25 26 27 | \DOC FIRST
\TYPE {FIRST : (tactic list -> tactic)}
\SYNOPSIS
Applies the first tactic in a tactic list which succeeds.
\KEYWORDS
tactical.
\DESCRIBE
When applied to a list of tactics {[T1;...;Tn]}, and a goal {g}, the tactical
{FIRST} tries applying the tactics to the goal until one succeeds. If the
first tactic which succeeds is {Tm}, then the effect is the same as just {Tm}.
Thus {FIRST} effectively behaves as follows:
{
FIRST [T1;...;Tn] = T1 ORELSE ... ORELSE Tn
}
\FAILURE
The application of {FIRST} to a tactic list never fails. The resulting
tactic fails iff all the component tactics do when applied to the goal,
or if the tactic list is empty.
\SEEALSO
EVERY, ORELSE.
\ENDDOC
|