Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
authorhaftmann
Thu, 18 Mar 2010 13:56:32 +0100
changeset 35818 680caf709510
parent 35817 d8b8527102f5
child 35819 8e81f71d0460
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
src/HOL/Matrix/Matrix.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle