--- a/doc-src/TutorialI/CTL/PDL.thy Fri Oct 06 01:21:17 2000 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy Fri Oct 06 12:31:53 2000 +0200
@@ -77,7 +77,8 @@
lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)"
apply(rule monoI)
-by(blast)
+apply blast
+done
text{*\noindent
in order to make sure it really has a least fixpoint.
@@ -174,7 +175,8 @@
*}
apply(rule ssubst[OF lfp_Tarski[OF mono_ef]])
-by(blast)
+apply(blast)
+done
text{*
The main theorem is proved in the familiar manner: induction followed by
@@ -183,5 +185,6 @@
theorem "mc f = {s. s \<Turnstile> f}";
apply(induct_tac f);
-by(auto simp add:EF_lemma);
+apply(auto simp add:EF_lemma);
+done;
(*<*)end(*>*)