diff -r 00fdd5c330ea -r a72ddfdbfca0 doc-src/TutorialI/CTL/PDL.thy
--- 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(*>*)