changeset 61890 | f6ded81f5690 |
parent 61832 | e15880ba58ac |
child 61955 | e96292f32c3c |
--- a/src/HOL/Library/Multiset.thy Fri Dec 18 14:23:11 2015 +0100 +++ b/src/HOL/Library/Multiset.thy Sat Dec 19 11:05:04 2015 +0100 @@ -1054,7 +1054,7 @@ lemma mset_map: "mset (map f xs) = image_mset f (mset xs)" by (induct xs) simp_all -permanent_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}" +global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}" defines mset_set = "folding.F (\<lambda>x M. {#x#} + M) {#}" by standard (simp add: fun_eq_iff ac_simps)