diff -r 91feea8e41e4 -r 22faf21db3df src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Jan 30 13:41:45 2009 +0000
+++ b/src/HOL/Matrix/Matrix.thy	Sat Jan 31 09:04:16 2009 +0100
@@ -1005,15 +1005,8 @@
   apply (subst foldseq_almostzero[of _ j])
   apply (simp add: prems)+
   apply (auto)
-  proof -
-    fix k
-    fix l
-    assume a:"~neg(int l - int i)"
-    assume b:"nat (int l - int i) = 0"
-    from a b have a: "l = i" by(insert not_neg_nat[of "int l - int i"], simp add: a b)
-    assume c: "i \<noteq> l"
-    from c a show "fmul (Rep_matrix A k j) e = 0" by blast
-  qed
+  apply (metis comm_monoid_add.mult_1 le_anti_sym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
+  done
 
 lemma mult_matrix_ext:
   assumes