# HG changeset patch # User wenzelm # Date 1313876178 -7200 # Node ID eda6aef75939301b754fa3b0e45eb084c591b72d # Parent 700008399ee5074279b930007936155def810870 odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??); diff -r 700008399ee5 -r eda6aef75939 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sat Aug 20 23:35:30 2011 +0200 +++ b/src/HOL/Library/Multiset.thy Sat Aug 20 23:36:18 2011 +0200 @@ -1598,7 +1598,7 @@ definition image_mset :: "('a \ 'b) \ 'a multiset \ 'b multiset" where "image_mset f = fold_mset (op + o single o f) {#}" -interpretation image_fun_commute: comp_fun_commute "op + o single o f" +interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f proof qed (simp add: add_ac fun_eq_iff) lemma image_mset_empty [simp]: "image_mset f {#} = {#}"