diff -r f1522b892a4c -r 5a176b8dda84 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Thu Aug 29 16:15:11 2002 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Fri Aug 30 16:42:45 2002 +0200
@@ -40,7 +40,7 @@
 by eliminates uses of assumption and done
 *}
 
-lemma imp_uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
+lemma imp_uncurry': "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
 apply (rule impI)
 apply (erule conjE)
 apply (drule mp)
@@ -353,7 +353,7 @@
 apply (simp add: Least_def LeastM_def)
 by (blast intro: some_equality order_antisym);
 
-theorem axiom_of_choice: "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
+theorem axiom_of_choice': "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
 apply (rule exI [of _  "\<lambda>x. SOME y. P x y"])
 by (blast intro: someI);