--- a/doc-src/TutorialI/CTL/CTL.thy Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Thu Nov 29 14:12:42 2001 +0100
@@ -106,7 +106,7 @@
*};
theorem AF_lemma1:
- "lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}";
+ "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}";
txt{*\noindent
In contrast to the analogous proof for @{term EF}, and just
@@ -304,7 +304,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: