1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 12 15:08:46 2013 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 12 18:09:17 2013 -0700
     1.3 @@ -499,7 +499,7 @@
     1.4    where "matrix f = (\<chi> i j. (f(axis j 1))$i)"
     1.5  
     1.6  lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
     1.7 -  by (simp add: linear_def matrix_vector_mult_def vec_eq_iff
     1.8 +  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
     1.9        field_simps setsum_right_distrib setsum_addf)
    1.10  
    1.11  lemma matrix_works: