doc-src/TutorialI/Rules/Basic.thy

 
 text {*
 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)
  apply assumption
 by (drule mp)

 (*both can be done by blast, which however hasn't been introduced yet*)
 lemma "[| P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x |] ==> (LEAST x. P(x)) = k";
 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);
 
 text{*end of Epsilon section*}