src/HOL/Matrix/Matrix.thy
changeset 16733 236dfafbeb63
parent 15481 fc075ae929e4
child 17915 e38947f9ba5e
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Thu Jul 07 12:36:56 2005 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Thu Jul 07 12:39:17 2005 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4  apply (simp add: one_matrix_def)
     1.5  apply (simplesubst RepAbs_matrix)
     1.6  apply (rule exI[of _ n], simp add: split_if)+
     1.7 -by (simp add: split_if, arith)
     1.8 +by (simp add: split_if)
     1.9  
    1.10  lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
    1.11  proof -