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