doc-src/TutorialI/Inductive/Star.thy

--- a/doc-src/TutorialI/Inductive/Star.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Inductive/Star.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -167,7 +167,7 @@
 lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
 apply(erule rtc.induct);
  apply blast;
-apply(blast intro:rtc_step)
+apply(blast intro: rtc_step)
 done
 
 end