--- a/src/HOL/Library/DAList_Multiset.thy Sun Sep 23 21:49:31 2018 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy Mon Sep 24 14:30:09 2018 +0200
@@ -372,7 +372,7 @@
end
-\<comment> \<open>we cannot use \<open>\<lambda>a n. (+) (a * n)\<close> for folding, since \<open>( * )\<close> is not defined in \<open>comm_monoid_add\<close>\<close>
+\<comment> \<open>we cannot use \<open>\<lambda>a n. (+) (a * n)\<close> for folding, since \<open>(*)\<close> is not defined in \<open>comm_monoid_add\<close>\<close>
lemma sum_mset_Bag[code]: "sum_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((+) a) ^^ n)) 0 ms"
unfolding sum_mset.eq_fold
apply (rule comp_fun_commute.DAList_Multiset_fold)
@@ -380,8 +380,8 @@
apply (auto simp: ac_simps)
done
-\<comment> \<open>we cannot use \<open>\<lambda>a n. ( * ) (a ^ n)\<close> for folding, since \<open>(^)\<close> is not defined in \<open>comm_monoid_mult\<close>\<close>
-lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((( * ) a) ^^ n)) 1 ms"
+\<comment> \<open>we cannot use \<open>\<lambda>a n. (*) (a ^ n)\<close> for folding, since \<open>(^)\<close> is not defined in \<open>comm_monoid_mult\<close>\<close>
+lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((*) a) ^^ n)) 1 ms"
unfolding prod_mset.eq_fold
apply (rule comp_fun_commute.DAList_Multiset_fold)
apply unfold_locales