# HG changeset patch
# User huffman
# Date 1313079075 25200
# Node ID d26a45f3c8357981184f739a14d81c8673fb5bb0
# Parent  ae2906662eeccac1248f254e5c84c07814471df2
remove lemma stupid_ext

diff -r ae2906662eec -r d26a45f3c835 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 13:24:49 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 09:11:15 2011 -0700
@@ -866,7 +866,7 @@
     obtain g where g: "linear g" "g o op *v A = id" by blast
     have "matrix g ** A = mat 1"
       unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
-      using g(2) by (simp add: o_def id_def stupid_ext)
+      using g(2) by (simp add: fun_eq_iff)
     then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast}
   ultimately show ?thesis by blast
 qed
@@ -894,7 +894,7 @@
     have "A ** (matrix g) = mat 1"
       unfolding matrix_eq  matrix_vector_mul_lid
         matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
-      using g(2) unfolding o_def stupid_ext[symmetric] id_def
+      using g(2) unfolding o_def fun_eq_iff id_def
       .
     hence "\<exists>B. A ** (B::real^'m^'n) = mat 1" by blast
   }
diff -r ae2906662eec -r d26a45f3c835 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 11 13:24:49 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 11 09:11:15 2011 -0700
@@ -41,9 +41,6 @@
 end
 *}
 
-lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
-  by auto
-
 lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
   by (simp add: vec_nth_inject [symmetric] fun_eq_iff)