src/HOL/List.thy

 lemma (in monoid_add) listsum_map_filter:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
   shows "listsum (map f (filter P xs)) = listsum (map f xs)"
   using assms by (induct xs) auto
 
-lemma (in monoid_add) distinct_listsum_conv_Setsum:
+lemma (in comm_monoid_add) distinct_listsum_conv_Setsum:
   "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
   by (induct xs) simp_all
 
 lemma listsum_eq_0_nat_iff_nat [simp]:
   "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"