/usr/share/hol88-2.02.19940316/help/ENTRIES/REPEATC.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 | \DOC REPEATC
\TYPE {REPEATC : (conv -> conv)}
\SYNOPSIS
Repeatedly apply a conversion (zero or more times) until it fails.
\KEYWORDS
conversional.
\DESCRIBE
If {c} is a conversion effects a transformation of a term {t} to a term {t'},
that is if {c} maps {t} to the theorem {|- t = t`}, then {REPEATC c} is the
conversion that repeats this transformation as often as possible. More
exactly, if {c} maps the term {"ti"} to {|- ti=t(i+1)} for {i} from {1} to {n},
but fails when applied to the {n+1}th term {"t(n+1)"}, then {REPEATC c "t1"}
returns {|- t1 = t(n+1)}. And if {c "t"} fails, them {REPEATC c "t"} returns
{|- t = t}.
\FAILURE
Never fails, but can diverge if the supplied conversion never fails.
\ENDDOC
|