diff -r 2f5edb146f7e -r 1f073030b97a doc-src/TutorialI/Overview/Sets.thy
--- a/doc-src/TutorialI/Overview/Sets.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Overview/Sets.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -102,7 +102,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{*