1.1 --- a/src/HOL/Matrix/Matrix.thy Sat Mar 17 11:59:59 2012 +0100
1.2 +++ b/src/HOL/Matrix/Matrix.thy Sat Mar 17 12:00:11 2012 +0100
1.3 @@ -64,7 +64,7 @@
1.4
1.5 lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)"
1.6 apply (rule ext)+
1.7 - by (simp add: transpose_infmatrix_def)
1.8 + by simp
1.9
1.10 lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)"
1.11 apply (rule Abs_matrix_inverse)
1.12 @@ -836,7 +836,7 @@
1.13 by (simp add: zero_matrix_def)
1.14
1.15 lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"
1.16 -apply (simp add: transpose_matrix_def transpose_infmatrix_def zero_matrix_def RepAbs_matrix)
1.17 +apply (simp add: transpose_matrix_def zero_matrix_def RepAbs_matrix)
1.18 apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
1.19 apply (simp add: RepAbs_matrix)
1.20 done
1.21 @@ -1464,7 +1464,7 @@
1.22 definition "sup = combine_matrix sup"
1.23
1.24 instance
1.25 - by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
1.26 + by default (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def)
1.27
1.28 end
1.29