/usr/share/hol88-2.02.19940316/help/ENTRIES/THEN.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 28 29 30 31 32 33 34 35 | \DOC THEN
\TYPE {$THEN : (tactic -> tactic -> tactic)}
\SYNOPSIS
Applies two tactics in sequence.
\KEYWORDS
tactical.
\DESCRIBE
If {T1} and {T2} are tactics, {T1 THEN T2} is a tactic which applies {T1} to a
goal, then applies the tactic {T2} to all the subgoals generated. If {T1}
solves the goal then {T2} is never applied.
\FAILURE
The application of {THEN} to a pair of tactics never fails.
The resulting tactic fails if {T1} fails when applied to the goal, or if
{T2} does when applied to any of the resulting subgoals.
\COMMENTS
Although normally used to sequence tactics which generate a single subgoal,
it is worth remembering that it is sometimes useful to apply the same tactic
to multiple subgoals; sequences like the following:
{
EQ_TAC THENL [ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]]
}
\noindent can be replaced by the briefer:
{
EQ_TAC THEN ASM_REWRITE_TAC[]
}
\SEEALSO
EVERY, ORELSE, THENL.
\ENDDOC
|