1.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Dec 13 17:43:33 2000 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Dec 13 17:46:49 2000 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4  into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
     1.5  \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
     1.6  \begin{isabelle}%
     1.7 -\ \ \ \ \ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}%
     1.8 +\ \ \ \ \ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}%
     1.9  \end{isabelle}
    1.10  The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s},
    1.11  in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true