doc-src/TutorialI/CTL/PDL.thy

 First we prove monotonicity of the function inside @{term lfp}
 *}
 
 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.
 
 Now we can relate model checking and semantics. For the @{text EF} case we need

 txt{*\noindent
 The proof of the induction step is identical to the one for the base case:
 *}
 
 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
 @{text auto} augmented with the lemma as a simplification rule.
 *}
 
 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(*>*)