diff -r 9429f2e7d16a -r ef0b521698b7 doc-src/TutorialI/CTL/document/CTL.tex
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Mon Jan 29 19:24:17 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Mon Jan 29 22:25:45 2001 +0100
@@ -64,10 +64,10 @@
 \noindent
 In contrast to the analogous property for \isa{EF}, and just
 for a change, we do not use fixed point induction but a weaker theorem,
-\isa{lfp{\isacharunderscore}lowerbound}:
-\begin{isabelle}%
-\ \ \ \ \ f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S%
-\end{isabelle}
+also known in the literature (after David Park) as \emph{Park-induction}:
+\begin{center}
+\isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
+\end{center}
 The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
 a decision that clarification takes for us:%
 \end{isamarkuptxt}%