| changeset 11244 | ca1de97d67c8 |
| parent 11234 | 6902638af59e |
| child 11407 | 138919f1a135 |
--- 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