diff -r d04f57b91166 -r e123a50aa949 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Fri Feb 23 16:31:21 2001 +0100
+++ b/doc-src/TutorialI/Rules/Basic.thy	Mon Feb 26 10:41:24 2001 +0100
@@ -62,7 +62,34 @@
 also provable by simp (re-orients)
 *};
 
-lemma "\<lbrakk> x = f x; P (f x) (f x) x \<rbrakk> \<Longrightarrow> P x x x"
+text {*
+the subst method
+
+@{thm[display] mult_commute}
+\rulename{mult_commute}
+
+this would fail:
+apply (simp add: mult_commute) 
+*};
+
+
+lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y"
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
+apply (subst mult_commute) 
+txt{*
+@{subgoals[display,indent=0,margin=65]}
+*};
+oops
+
+(*exercise involving THEN*)
+lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y"
+apply (rule mult_commute [THEN ssubst]) 
+oops
+
+
+lemma "\<lbrakk>x = f x; triple (f x) (f x) x\<rbrakk> \<Longrightarrow> triple x x x"
 apply (erule ssubst) 
   --{* @{subgoals[display,indent=0,margin=65]} *}
 back --{* @{subgoals[display,indent=0,margin=65]} *}
@@ -72,7 +99,7 @@
 apply assumption
 done
 
-lemma "\<lbrakk> x = f x; P (f x) (f x) x \<rbrakk> \<Longrightarrow> P x x x"
+lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x"
 apply (erule ssubst, assumption)
 done
 
@@ -80,18 +107,18 @@
 or better still 
 *}
 
-lemma "\<lbrakk> x = f x; P (f x) (f x) x \<rbrakk> \<Longrightarrow> P x x x"
+lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x"
 by (erule ssubst)
 
 
-lemma "\<lbrakk> x = f x; P (f x) (f x) x \<rbrakk> \<Longrightarrow> P x x x"
-apply (erule_tac P="\<lambda>u. P u u x" in ssubst)
+lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x"
+apply (erule_tac P="\<lambda>u. triple u u x" in ssubst)
 apply (assumption)
 done
 
 
-lemma "\<lbrakk> x = f x; P (f x) (f x) x \<rbrakk> \<Longrightarrow> P x x x"
-by (erule_tac P="\<lambda>u. P u u x" in ssubst)
+lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x"
+by (erule_tac P="\<lambda>u. triple u u x" in ssubst)
 
 
 text {*
@@ -148,6 +175,14 @@
 *}
 
 
+text{*rule_tac, etc.*}
+
+
+lemma "P&Q"
+apply (rule_tac P=P and Q=Q in conjI)
+oops
+
+
 text{*Quantifiers*}