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: