Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/Divisibility.thy
changeset 36903 489c1fbbb028
parent 36278 6b330b1fa0c0
child 39302 d7728f65b353 
--- a/src/HOL/Algebra/Divisibility.thy	Wed May 12 22:33:10 2010 -0700
+++ b/src/HOL/Algebra/Divisibility.thy	Thu May 13 14:34:05 2010 +0200
@@ -2193,7 +2193,7 @@
 
   from csmset msubset
       have "fmset G bs = fmset G as + fmset G cs"
-      by (simp add: multiset_eq_conv_count_eq mset_le_def)
+      by (simp add: multiset_ext_iff mset_le_def)
   hence basc: "b \<sim> a \<otimes> c"
       by (rule fmset_wfactors_mult) fact+
isabelle