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