src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
changeset 44165 d26a45f3c835
parent 44140 2c10c35dd4be
child 44166 d12d89a66742
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 13:24:49 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 09:11:15 2011 -0700
     1.3 @@ -866,7 +866,7 @@
     1.4      obtain g where g: "linear g" "g o op *v A = id" by blast
     1.5      have "matrix g ** A = mat 1"
     1.6        unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
     1.7 -      using g(2) by (simp add: o_def id_def stupid_ext)
     1.8 +      using g(2) by (simp add: fun_eq_iff)
     1.9      then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast}
    1.10    ultimately show ?thesis by blast
    1.11  qed
    1.12 @@ -894,7 +894,7 @@
    1.13      have "A ** (matrix g) = mat 1"
    1.14        unfolding matrix_eq  matrix_vector_mul_lid
    1.15          matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
    1.16 -      using g(2) unfolding o_def stupid_ext[symmetric] id_def
    1.17 +      using g(2) unfolding o_def fun_eq_iff id_def
    1.18        .
    1.19      hence "\<exists>B. A ** (B::real^'m^'n) = mat 1" by blast
    1.20    }