| changeset 63524 | 4ec755485732 |
| parent 63410 | 9789ccc2a477 |
| child 63534 | 523b488b15c9 |
| child 63539 | 70d4d9e5707b |
--- a/src/HOL/Library/Multiset.thy Tue Jul 19 16:50:39 2016 +0200 +++ b/src/HOL/Library/Multiset.thy Wed Jul 20 13:51:38 2016 +0200 @@ -1612,7 +1612,7 @@ lemma mset_insort [simp]: "mset (insort x xs) = mset xs + {#x#}" by (induct xs) (simp_all add: ac_simps) -lemma mset_map: "mset (map f xs) = image_mset f (mset xs)" +lemma mset_map[simp]: "mset (map f xs) = image_mset f (mset xs)" by (induct xs) simp_all global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"