--- 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: