--- a/doc-src/TutorialI/Rules/Tacticals.thy Mon Jan 29 10:27:29 2001 +0100
+++ b/doc-src/TutorialI/Rules/Tacticals.thy Mon Jan 29 10:28:00 2001 +0100
@@ -32,10 +32,12 @@
prefer 3 --{* @{subgoals[display,indent=0,margin=65]} *}
oops
-lemma "thing1 \<and> thing2 \<and> thing3 \<and> thing4 \<and> thing5 \<and> thing6"
+lemma "bigsubgoal1 \<and> bigsubgoal2 \<and> bigsubgoal3 \<and> bigsubgoal4 \<and> bigsubgoal5 \<and> bigsubgoal6"
apply intro --{* @{subgoals[display,indent=0,margin=65]} *}
pr 2
-txt{* @{subgoals[display,indent=0,margin=65]} *}
+txt{* @{subgoals[display,indent=0,margin=65]}
+A total of 6 subgoals...
+*}
oops