# HG changeset patch
# User paulson
# Date 986803953 -7200
# Node ID ca1de97d67c86d2d898350f0946272d6008bdad8
# Parent  a9d4f354aba2025c88cb25524fdd6a8d78a2da4a
extra display

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