# HG changeset patch
# User wenzelm
# Date 1007562996 -3600
# Node ID 2fa13b49997597aed3064b5efab5aff0a54e6192
# Parent  23bd419144ebcbae4d25488a62c2c73affb292ba
adapted intr/elim uses;

diff -r 23bd419144eb -r 2fa13b499975 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Wed Dec 05 14:32:10 2001 +0100
+++ b/doc-src/TutorialI/Rules/Basic.thy	Wed Dec 05 15:36:36 2001 +0100
@@ -150,7 +150,7 @@
 lemma "\<lbrakk>\<not>(P\<longrightarrow>Q); \<not>(R\<longrightarrow>Q)\<rbrakk> \<Longrightarrow> R"
 apply (erule_tac Q="R\<longrightarrow>Q" in contrapos_np)
 	--{* @{subgoals[display,indent=0,margin=65]} *}
-apply intro
+apply (intro impI)
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 by (erule notE)
 
@@ -160,7 +160,7 @@
 *};
 
 lemma "(P \<or> Q) \<and> R \<Longrightarrow> P \<or> Q \<and> R"
-apply intro
+apply (intro conjI disjCI)
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 
 apply (elim conjE disjE)
@@ -211,7 +211,7 @@
 
 text{*rename_tac*}
 lemma "x < y \<Longrightarrow> \<forall>x y. P x (f y)"
-apply intro
+apply (intro allI)
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 apply (rename_tac v w)
 	--{* @{subgoals[display,indent=0,margin=65]} *}
@@ -361,21 +361,22 @@
 
 
 lemma "(\<exists>x. P x) \<or> (\<exists>x. Q x) \<Longrightarrow> \<exists>x. P x \<or> Q x"
-apply elim
- apply intro
+apply (elim exE disjE)
+ apply (intro exI disjCI)
  apply assumption
 apply (intro exI disjI2) (*or else we get disjCI*)
 apply assumption
 done
 
 lemma "(P\<longrightarrow>Q) \<or> (Q\<longrightarrow>P)"
-apply intro
-apply elim
+apply (intro disjCI impI)
+apply (elim notE)
+apply (intro impI)
 apply assumption
 done
 
 lemma "(P\<or>Q)\<and>(P\<or>R) \<Longrightarrow> P \<or> (Q\<and>R)"
-apply intro
+apply (intro disjCI conjI)
 apply (elim conjE disjE)
 apply blast
 apply blast
diff -r 23bd419144eb -r 2fa13b499975 doc-src/TutorialI/Rules/Forward.thy
--- a/doc-src/TutorialI/Rules/Forward.thy	Wed Dec 05 14:32:10 2001 +0100
+++ b/doc-src/TutorialI/Rules/Forward.thy	Wed Dec 05 15:36:36 2001 +0100
@@ -117,7 +117,7 @@
 *}
 
 lemma "2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)"
-apply intro
+apply (intro notI)
 txt{*
 before using arg_cong
 @{subgoals[display,indent=0,margin=65]}
diff -r 23bd419144eb -r 2fa13b499975 doc-src/TutorialI/Rules/Tacticals.thy
--- a/doc-src/TutorialI/Rules/Tacticals.thy	Wed Dec 05 14:32:10 2001 +0100
+++ b/doc-src/TutorialI/Rules/Tacticals.thy	Wed Dec 05 15:36:36 2001 +0100
@@ -17,23 +17,23 @@
 
 text{*exercise: what's going on here?*}
 lemma "\<lbrakk>P\<and>Q\<longrightarrow>R; P\<longrightarrow>Q; P\<rbrakk> \<Longrightarrow> R"
-by (drule mp, intro?, assumption+)+
+by (drule mp, (intro conjI)?, assumption+)+
 
 text{*defer and prefer*}
 
 lemma "hard \<and> (P \<or> ~P) \<and> (Q\<longrightarrow>Q)"
-apply intro   --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (intro conjI)   --{* @{subgoals[display,indent=0,margin=65]} *}
 defer 1   --{* @{subgoals[display,indent=0,margin=65]} *}
 apply blast+   --{* @{subgoals[display,indent=0,margin=65]} *}
 oops
 
 lemma "ok1 \<and> ok2 \<and> doubtful"
-apply intro   --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (intro conjI)   --{* @{subgoals[display,indent=0,margin=65]} *}
 prefer 3   --{* @{subgoals[display,indent=0,margin=65]} *}
 oops
 
 lemma "bigsubgoal1 \<and> bigsubgoal2 \<and> bigsubgoal3 \<and> bigsubgoal4 \<and> bigsubgoal5 \<and> bigsubgoal6"
-apply intro   --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (intro conjI)   --{* @{subgoals[display,indent=0,margin=65]} *}
 txt{* @{subgoals[display,indent=0,margin=65]} 
 A total of 6 subgoals...
 *}
@@ -44,7 +44,7 @@
 (*needed??*)
 
 lemma "(P\<or>Q) \<and> (R\<or>S) \<Longrightarrow> PP"
-apply elim
+apply (elim conjE disjE)
 oops
 
 lemma "((P\<or>Q) \<and> R) \<and> (Q \<and> (P\<or>S)) \<Longrightarrow> PP"