diff -r a9d4f354aba2 -r ca1de97d67c8 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Mon Apr 09 10:12:12 2001 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Mon Apr 09 10:12:33 2001 +0200
@@ -264,6 +264,7 @@
 apply (erule exE) 
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 apply (rule_tac x="k*ka" in exI) 
+	--{* @{subgoals[display,indent=0,margin=65]} *}
 apply simp
 done