src/HOL/Analysis/Cartesian_Euclidean_Space.thy
 changeset 66804 3f9bb52082c4 parent 66447 a1f5c5c26fa6 child 67155 9e5b05d54f9d
1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Oct 08 22:28:20 2017 +0200
1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Oct 08 22:28:20 2017 +0200
1.3 @@ -518,14 +518,14 @@
1.5  lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
1.6    apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
1.7 -  apply (subst sum.commute)
1.8 +  apply (subst sum.swap)
1.9    apply simp
1.10    done
1.12  lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
1.13    apply (vector matrix_matrix_mult_def matrix_vector_mult_def
1.14      sum_distrib_left sum_distrib_right mult.assoc)
1.15 -  apply (subst sum.commute)
1.16 +  apply (subst sum.swap)
1.17    apply simp
1.18    done
1.20 @@ -556,7 +556,7 @@
1.22  lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
1.23    apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps)
1.24 -  apply (subst sum.commute)
1.25 +  apply (subst sum.swap)
1.26    apply simp
1.27    done
1.29 @@ -659,7 +659,7 @@