/usr/share/hol88-2.02.19940316/help/ENTRIES/THENC.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 | \DOC THENC
\TYPE {$THENC : (conv -> conv -> conv)}
\SYNOPSIS
Applies two conversions in sequence.
\KEYWORDS
conversional.
\DESCRIBE
If the conversion {c1} returns {|- t = t'} when applied to a term {"t"}, and
{c2} returns {|- t' = t''} when applied to {"t'"}, then the composite
conversion {(c1 THENC c2) "t"} returns {|- t = t''}. That is, {(c1 THENC c2)
"t"} has the effect of transforming the term {"t"} first with the conversion
{c1} and then with the conversion {c2}.
\FAILURE
{(c1 THENC c2) "t"} fails if either the conversion {c1} fails when applied to
{"t"}, or if {c1 "t"} succeeds and returns {|- t = t'} but {c2} fails when
applied to {"t'"}. {(c1 THENC c2) "t"} may also fail if either of {c1} or {c2}
is not, in fact, a conversion (i.e. a function that maps a term {t} to a
theorem {|- t = t'}).
\SEEALSO
EVERY_CONV.
\ENDDOC
|