author nipkow Thu, 11 Jan 2001 11:47:57 +0100 changeset 10866 cf8956f49499 parent 10865 18927bcf7aed child 10867 bda1701848cd
*** empty log message ***
--- 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}%
The proof is again pointwise and then by contraposition:%