# HG changeset patch
# User haftmann
# Date 1268916992 -3600
# Node ID 680caf709510e6656b092451550ac0b83e27b757
# Parent  d8b8527102f56db0c4b7f3fe37685ccc469c5913
dropped odd interpretation of comm_monoid_mult into comm_monoid_add

diff -r d8b8527102f5 -r 680caf709510 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Thu Mar 18 13:56:32 2010 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Thu Mar 18 13:56:32 2010 +0100
@@ -1015,7 +1015,7 @@
   apply (subst foldseq_almostzero[of _ j])
   apply (simp add: assms)+
   apply (auto)
-  apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
+  apply (metis add_0 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
   done
 
 lemma mult_matrix_ext: