extra display
authorpaulson
Mon, 09 Apr 2001 10:12:33 +0200
changeset 11244 ca1de97d67c8
parent 11243 a9d4f354aba2
child 11245 3d9d25a3375b
extra display
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