# HG changeset patch
# User paulson
# Date 980261185 -3600
# Node ID f2c1a280f1e3921de0ad0cda0ebb242f24bc601e
# Parent  cda180b1e2e0b35e6edf2fe0955a9bf49ad03a5d
added a "pr" example; tidied

diff -r cda180b1e2e0 -r f2c1a280f1e3 doc-src/TutorialI/Rules/Tacticals.thy
--- a/doc-src/TutorialI/Rules/Tacticals.thy	Mon Jan 22 17:26:19 2001 +0100
+++ b/doc-src/TutorialI/Rules/Tacticals.thy	Tue Jan 23 15:46:25 2001 +0100
@@ -1,22 +1,22 @@
 theory Tacticals = Main:
 
 text{*REPEAT*}
-lemma "\<lbrakk>(P\<longrightarrow>Q); (Q\<longrightarrow>R); (R\<longrightarrow>S); P\<rbrakk> \<Longrightarrow> S"
+lemma "\<lbrakk>P\<longrightarrow>Q; Q\<longrightarrow>R; R\<longrightarrow>S; P\<rbrakk> \<Longrightarrow> S"
 apply (drule mp, assumption)
 apply (drule mp, assumption)
 apply (drule mp, assumption)
 apply (assumption)
 done
 
-lemma "\<lbrakk>(P\<longrightarrow>Q); (Q\<longrightarrow>R); (R\<longrightarrow>S); P\<rbrakk> \<Longrightarrow> S"
+lemma "\<lbrakk>P\<longrightarrow>Q; Q\<longrightarrow>R; R\<longrightarrow>S; P\<rbrakk> \<Longrightarrow> S"
 by (drule mp, assumption)+
 
 text{*ORELSE with REPEAT*}
-lemma "\<lbrakk>(Q\<longrightarrow>R); (P\<longrightarrow>Q); x<#5\<longrightarrow>P;  Suc x < #5\<rbrakk> \<Longrightarrow> R" 
+lemma "\<lbrakk>Q\<longrightarrow>R; P\<longrightarrow>Q; x<#5\<longrightarrow>P;  Suc x < #5\<rbrakk> \<Longrightarrow> R" 
 by (drule mp, (assumption|arith))+
 
 text{*exercise: what's going on here?*}
-lemma "\<lbrakk>(P\<and>Q\<longrightarrow>R); (P\<longrightarrow>Q); P\<rbrakk> \<Longrightarrow> R"
+lemma "\<lbrakk>P\<and>Q\<longrightarrow>R; P\<longrightarrow>Q; P\<rbrakk> \<Longrightarrow> R"
 by (drule mp, intro?, assumption+)+
 
 text{*defer and prefer*}
@@ -32,6 +32,12 @@
 prefer 3   --{* @{subgoals[display,indent=0,margin=65]} *}
 oops
 
+lemma "thing1 \<and> thing2 \<and> thing3 \<and> thing4 \<and> thing5 \<and> thing6"
+apply intro   --{* @{subgoals[display,indent=0,margin=65]} *}
+pr 2  
+txt{* @{subgoals[display,indent=0,margin=65]} *}
+oops
+
 
 
 (*needed??*)