src/HOL/Matrix/Matrix.thy

 proof
   fix A B C :: "('a :: lordered_ring) matrix"
   show "A * B * C = A * (B * C)"
     apply (simp add: times_matrix_def)
     apply (rule mult_matrix_assoc)
-    apply (simp_all add: associative_def ring_eq_simps)
+    apply (simp_all add: associative_def ring_simps)
     done
   show "(A + B) * C = A * C + B * C"
     apply (simp add: times_matrix_def plus_matrix_def)
     apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec])
-    apply (simp_all add: associative_def commutative_def ring_eq_simps)
+    apply (simp_all add: associative_def commutative_def ring_simps)
     done
   show "A * (B + C) = A * B + A * C"
     apply (simp add: times_matrix_def plus_matrix_def)
     apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
-    apply (simp_all add: associative_def commutative_def ring_eq_simps)
+    apply (simp_all add: associative_def commutative_def ring_simps)
     done  
   show "abs A = sup A (-A)" 
     by (simp add: abs_matrix_def)
   assume a: "A \<le> B"
   assume b: "0 \<le> C"

 constdefs
   scalar_mult :: "('a::lordered_ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix"
   "scalar_mult a m == apply_matrix (op * a) m"
 
 lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" 
-  by (simp add: scalar_mult_def)
+by (simp add: scalar_mult_def)
 
 lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"
-  by (simp add: scalar_mult_def apply_matrix_add ring_eq_simps)
+by (simp add: scalar_mult_def apply_matrix_add ring_simps)
 
 lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)" 
-  by (simp add: scalar_mult_def)
+by (simp add: scalar_mult_def)
 
 lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"
-  apply (subst Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply (auto)
-  done
+apply (subst Rep_matrix_inject[symmetric])
+apply (rule ext)+
+apply (auto)
+done
 
 lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
-  by (simp add: minus_matrix_def)
+by (simp add: minus_matrix_def)
 
 lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
-  by (simp add: abs_lattice sup_matrix_def)
+by (simp add: abs_lattice sup_matrix_def)
 
 end