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 39302 d7728f65b353
parent 36903 489c1fbbb028
child 41413 64cd30d6b0b8 
--- a/src/HOL/Algebra/Divisibility.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -2193,7 +2193,7 @@
 
   from csmset msubset
       have "fmset G bs = fmset G as + fmset G cs"
-      by (simp add: multiset_ext_iff mset_le_def)
+      by (simp add: multiset_eq_iff mset_le_def)
   hence basc: "b \<sim> a \<otimes> c"
       by (rule fmset_wfactors_mult) fact+
isabelle