1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -418,7 +418,7 @@
     1.4    by (simp add: matrix_vector_mult_def inner_vec_def)
     1.5  
     1.6  lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
     1.7 -  apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
     1.8 +  apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib ac_simps)
     1.9    apply (subst setsum.commute)
    1.10    apply simp
    1.11    done
    1.12 @@ -525,7 +525,7 @@
    1.13    apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
    1.14      setsum_left_distrib setsum_right_distrib)
    1.15    apply (subst setsum.commute)
    1.16 -  apply (auto simp add: mult_ac)
    1.17 +  apply (auto simp add: ac_simps)
    1.18    done
    1.19  
    1.20  lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
    1.21 @@ -1221,7 +1221,7 @@
    1.22    unfolding UNIV_2 by simp
    1.23  
    1.24  lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
    1.25 -  unfolding UNIV_3 by (simp add: add_ac)
    1.26 +  unfolding UNIV_3 by (simp add: ac_simps)
    1.27  
    1.28  instantiation num1 :: cart_one
    1.29  begin