changeset 54864 | a064732223ad |
parent 54230 | b1d955791529 |
child 57512 | cc97b347b301 |
--- a/src/HOL/Matrix_LP/Matrix.thy Wed Dec 25 17:39:06 2013 +0100 +++ b/src/HOL/Matrix_LP/Matrix.thy Wed Dec 25 17:39:07 2013 +0100 @@ -1270,7 +1270,7 @@ 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)"