--- a/doc-src/TutorialI/CTL/PDL.thy Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy Fri Jan 18 18:30:19 2002 +0100
@@ -174,7 +174,7 @@
theorem "mc f = {s. s \<Turnstile> f}"
apply(induct_tac f)
-apply(auto simp add:EF_lemma)
+apply(auto simp add: EF_lemma)
done
text{*