--- a/doc-src/TutorialI/CTL/document/CTL.tex Sat Jan 06 11:27:09 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Sat Jan 06 12:39:05 2001 +0100
@@ -300,7 +300,7 @@
Model checking \isa{EU} is again a least fixed point construction:
\begin{isabelle}%
-\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}%
+\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}%
\end{isabelle}
\begin{exercise}