| changeset 42809 | 5b45125b15ba |
| parent 41505 | 6d19301074cf |
| child 42871 | 1c0b99f950d9 |
--- a/src/HOL/Library/Multiset.thy Sat May 14 00:32:16 2011 +0200 +++ b/src/HOL/Library/Multiset.thy Sat May 14 18:26:25 2011 +0200 @@ -1599,7 +1599,7 @@ "image_mset f = fold_mset (op + o single o f) {#}" interpretation image_left_comm: fun_left_comm "op + o single o f" -proof qed (simp add: add_ac) +proof qed (simp add: add_ac fun_eq_iff) lemma image_mset_empty [simp]: "image_mset f {#} = {#}" by (simp add: image_mset_def)