diff -r 39c37e16f748 -r 2c02a8054616 doc-src/TutorialI/CTL/document/CTL.tex
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Tue May 16 18:31:46 2006 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Tue May 16 20:28:02 2006 +0200
@@ -141,9 +141,9 @@
 for a change, we do not use fixed point induction.  Park-induction,
 named after David Park, is weaker but sufficient for this proof:
 \begin{center}
-\isa{f\ S\ {\isasymle}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymle}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
+\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\ {\isasymle}\ S} is proved pointwise,
+The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
 a decision that \isa{auto} takes for us:%
 \end{isamarkuptxt}%
 \isamarkuptrue%