--- a/doc-src/TutorialI/CTL/document/CTL.tex Sat Mar 18 18:33:40 2006 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Sat Mar 18 18:33:49 2006 +0100
@@ -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\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
+\isa{f\ S\ {\isasymle}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymle}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
\end{center}
-The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
+The instance of the premise \isa{f\ S\ {\isasymle}\ S} is proved pointwise,
a decision that \isa{auto} takes for us:%
\end{isamarkuptxt}%
\isamarkuptrue%