src/HOL/List.thy
changeset 51738 9e4220605179
parent 51717 9e7d1c139569
child 51875 dafd097dd1f4
     1.1 --- a/src/HOL/List.thy	Tue Apr 23 11:14:50 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Apr 23 11:14:51 2013 +0200
     1.3 @@ -3376,7 +3376,7 @@
     1.4    shows "listsum (map f (filter P xs)) = listsum (map f xs)"
     1.5    using assms by (induct xs) auto
     1.6  
     1.7 -lemma (in monoid_add) distinct_listsum_conv_Setsum:
     1.8 +lemma (in comm_monoid_add) distinct_listsum_conv_Setsum:
     1.9    "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
    1.10    by (induct xs) simp_all
    1.11