src/HOL/Matrix/Matrix.thy

--- a/src/HOL/Matrix/Matrix.thy	Thu Jul 07 12:36:56 2005 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Thu Jul 07 12:39:17 2005 +0200
@@ -131,7 +131,7 @@
 apply (simp add: one_matrix_def)
 apply (simplesubst RepAbs_matrix)
 apply (rule exI[of _ n], simp add: split_if)+
-by (simp add: split_if, arith)
+by (simp add: split_if)
 
 lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
 proof -