# HG changeset patch
# User nipkow
# Date 979210077 -3600
# Node ID cf8956f494991e0943b9aa595ae7c3e924ddb6d2
# Parent  18927bcf7aed10b545d598d804c2615214860b95
*** empty log message ***

diff -r 18927bcf7aed -r cf8956f49499 doc-src/TutorialI/CTL/CTL.thy
--- 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:
diff -r 18927bcf7aed -r cf8956f49499 doc-src/TutorialI/CTL/document/CTL.tex
--- 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:%