1.1 --- a/src/HOL/Matrix/ComputeNumeral.thy	Sat Mar 17 11:59:59 2012 +0100
     1.2 +++ b/src/HOL/Matrix/ComputeNumeral.thy	Sat Mar 17 12:00:11 2012 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5  (* multiplication for bit strings *) 
     1.6  lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def)
     1.7 -lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min)
     1.8 +lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute) simp 
     1.9  lemma multb0x: "(Int.Bit0 x) * y = Int.Bit0 (x * y)" by (rule mult_Bit0)
    1.10  lemma multxb0: "x * (Int.Bit0 y) = Int.Bit0 (x * y)" unfolding Bit0_def by simp
    1.11  lemma multb1: "(Int.Bit1 x) * (Int.Bit1 y) = Int.Bit1 (Int.Bit0 (x * y) + x + y)"

     2.1 --- a/src/HOL/Matrix/Matrix.thy	Sat Mar 17 11:59:59 2012 +0100
     2.2 +++ b/src/HOL/Matrix/Matrix.thy	Sat Mar 17 12:00:11 2012 +0100
     2.3 @@ -64,7 +64,7 @@
     2.4  
     2.5  lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)"
     2.6    apply (rule ext)+
     2.7 -  by (simp add: transpose_infmatrix_def)
     2.8 +  by simp
     2.9  
    2.10  lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)"
    2.11  apply (rule Abs_matrix_inverse)
    2.12 @@ -836,7 +836,7 @@
    2.13    by (simp add: zero_matrix_def)
    2.14  
    2.15  lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"
    2.16 -apply (simp add: transpose_matrix_def transpose_infmatrix_def zero_matrix_def RepAbs_matrix)
    2.17 +apply (simp add: transpose_matrix_def zero_matrix_def RepAbs_matrix)
    2.18  apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
    2.19  apply (simp add: RepAbs_matrix)
    2.20  done
    2.21 @@ -1464,7 +1464,7 @@
    2.22  definition "sup = combine_matrix sup"
    2.23  
    2.24  instance
    2.25 -  by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
    2.26 +  by default (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def)
    2.27  
    2.28  end
    2.29