--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Nov 16 18:45:57 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Nov 16 19:14:23 2012 +0100
@@ -398,8 +398,6 @@
then show "h = g" by (simp add: ext)
qed
-lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis
-
subsection {* Interlude: Some properties of real sets *}
lemma seq_mono_lemma: assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n" and "\<forall>n \<ge> m. e n <= e m"
@@ -1377,8 +1375,6 @@
finally show ?thesis .
qed
-lemma choice_iff': "(\<forall>x<d. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x<d. P x (f x))" by metis
-
lemma lambda_skolem': "(\<forall>i<DIM('a::euclidean_space). \<exists>x. P i x) \<longleftrightarrow>
(\<exists>x::'a. \<forall>i<DIM('a). P i (x$$i))" (is "?lhs \<longleftrightarrow> ?rhs")
proof -