src/HOL/Matrix_LP/Matrix.thy

   shows
   "transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)"
   apply (simp add: Rep_matrix_inject[THEN sym])
   apply (rule ext)+
   using assms
-  apply (simp add: Rep_mult_matrix max_ac)
+  apply (simp add: Rep_mult_matrix ac_simps)
   done
 
 lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"
 apply (simp add:  Rep_matrix_inject[THEN sym])
 apply (rule ext)+