# HG changeset patch
# User paulson
# Date 1007640067 -3600
# Node ID 2884148a9fe94612d8e33af79397ac8c7536d9e1
# Parent  70ebb59264f1ab80779884885afe881832e1c853
intro and elim now require arguments

diff -r 70ebb59264f1 -r 2884148a9fe9 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Thu Dec 06 13:00:25 2001 +0100
+++ b/doc-src/TutorialI/Rules/Basic.thy	Thu Dec 06 13:01:07 2001 +0100
@@ -160,7 +160,7 @@
 *};
 
 lemma "(P \<or> Q) \<and> R \<Longrightarrow> P \<or> Q \<and> R"
-apply (intro conjI disjCI)
+apply (intro disjCI conjI)
 	--{* @{subgoals[display,indent=0,margin=65]} *}
 
 apply (elim conjE disjE)
@@ -362,9 +362,9 @@
 
 lemma "(\<exists>x. P x) \<or> (\<exists>x. Q x) \<Longrightarrow> \<exists>x. P x \<or> Q x"
 apply (elim exE disjE)
- apply (intro exI disjCI)
+ apply (intro exI disjI1)
  apply assumption
-apply (intro exI disjI2) (*or else we get disjCI*)
+apply (intro exI disjI2)
 apply assumption
 done
 
diff -r 70ebb59264f1 -r 2884148a9fe9 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Thu Dec 06 13:00:25 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Thu Dec 06 13:01:07 2001 +0100
@@ -465,7 +465,7 @@
 R"\isanewline
 \isacommand{apply}\ (erule_tac\ Q = "R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
 contrapos_np)\isanewline
-\isacommand{apply}\ intro\isanewline
+\isacommand{apply}\ (intro\ impI)\isanewline
 \isacommand{by}\ (erule\ notE)
 \end{isabelle}
 %
@@ -482,7 +482,7 @@
 conclusion.
 
 We can now apply introduction rules.  We use the \methdx{intro} method, which
-repeatedly  applies built-in introduction rules.  Here its effect is equivalent
+repeatedly applies the given introduction rules.  Here its effect is equivalent
 to \isa{rule impI}.
 \begin{isabelle}
 \ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\
@@ -514,16 +514,16 @@
 \begin{isabelle}
 \isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\
 \isasymLongrightarrow\ P\ \isasymor\ (Q\ \isasymand\ R)"\isanewline
-\isacommand{apply}\ intro\isanewline
+\isacommand{apply}\ (intro\ disjCI\ conjI)\isanewline
 \isacommand{apply}\ (elim\ conjE\ disjE)\isanewline
 \ \isacommand{apply}\ assumption
 \isanewline
 \isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI)
 \end{isabelle}
 %
-The first proof step applies the \isa{intro} method, which repeatedly  uses
-built-in introduction rules.  Among these are \isa{disjCI}, which creates
-the negative assumption 
+The first proof step uses \isa{intro} to apply
+the introduction rules \isa{disjCI} and \isa{conjI}.  The resulting
+subgoal has the negative assumption 
 \hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}.  
 
 \begin{isabelle}
@@ -1052,7 +1052,7 @@
 \begin{isabelle}
 \isacommand{lemma}\ "x\ <\ y\ \isasymLongrightarrow \ \isasymforall x\ y.\ P\ x\
 (f\ y)"\isanewline
-\isacommand{apply}\ intro\isanewline
+\isacommand{apply}\ (intro allI)\isanewline
 \ 1.\ \isasymAnd xa\ ya.\ x\ <\ y\ \isasymLongrightarrow \ P\ xa\ (f\ ya)
 \end{isabelle}
 %
@@ -2054,7 +2054,7 @@
 \begin{isabelle}
 \isacommand{lemma}\ "2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
 \ Suc(u*n)"\isanewline
-\isacommand{apply}\ intro\isanewline
+\isacommand{apply}\ (intro\ notI)\isanewline
 \ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
 \end{isabelle}
 %
@@ -2336,10 +2336,6 @@
 
 In the following example, the first subgoal looks hard, while the others
 look as if \isa{blast} alone could prove them:
-%\begin{isabelle}
-%\isacommand{lemma}\ "hard\ \isasymand \ (P\ \isasymor \ \isachartilde P)\ \isasymand \ (Q\isasymlongrightarrow Q)"\isanewline
-%\isacommand{apply}\ intro
-%\end{isabelle}
 \begin{isabelle}
 \ 1.\ hard\isanewline
 \ 2.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline