1.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Mon Nov 27 11:06:28 2000 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Mon Nov 27 16:40:56 2000 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4  \noindent
     1.5  Simplification leaves us with the following first subgoal
     1.6  \begin{isabelle}%
     1.7 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A%
     1.8 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A%
     1.9  \end{isabelle}
    1.10  which is proved by \isa{lfp}-induction:%
    1.11  \end{isamarkuptxt}%