# HG changeset patch
# User paulson
# Date 980760480 -3600
# Node ID c36733b147e8adb9440b8e01d79bb79064284c0d
# Parent  616bcfc7b8483cb74558502847b64f5cb0c6122a
fixed the pr example

diff -r 616bcfc7b848 -r c36733b147e8 doc-src/TutorialI/Rules/Tacticals.thy
--- 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