--- a/doc-src/TutorialI/CTL/document/CTL.tex Thu Nov 09 11:58:43 2006 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Thu Nov 09 11:58:45 2006 +0100
@@ -141,7 +141,7 @@
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,
a decision that \isa{auto} takes for us:%