--- a/doc-src/TutorialI/CTL/CTL.thy Thu Jan 11 11:37:03 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Thu Jan 11 11:47:57 2001 +0100
@@ -302,8 +302,7 @@
At last we can prove the opposite direction of @{thm[source]AF_lemma1}:
*};
-theorem AF_lemma2:
-"{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
+theorem AF_lemma2: "{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
txt{*\noindent
The proof is again pointwise and then by contraposition:
--- a/doc-src/TutorialI/CTL/document/CTL.tex Thu Jan 11 11:37:03 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Thu Jan 11 11:47:57 2001 +0100
@@ -240,8 +240,7 @@
\begin{isamarkuptext}%
At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma{\isadigit{1}}}:%
\end{isamarkuptext}%
-\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline
-{\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}%
+\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
The proof is again pointwise and then by contraposition:%