src/HOL/List.thy
changeset 46383 26c422552cfe
parent 46317 80dccedd6c14
child 46396 da32cf32c0c7
     1.1 --- a/src/HOL/List.thy	Tue Jan 31 15:13:18 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Jan 31 15:39:45 2012 +0100
     1.3 @@ -5674,6 +5674,11 @@
     1.4    "Pow (set (x # xs)) = (let A = Pow (set xs) in A \<union> insert x ` A)"
     1.5    by (simp_all add: Pow_insert Let_def)
     1.6  
     1.7 +text {* Further operations on sets *}
     1.8 +
     1.9 +lemma setsum_code [code]:
    1.10 +  "setsum f (set xs) = listsum (map f (remdups xs))"
    1.11 +by (simp add: listsum_distinct_conv_setsum_set)
    1.12  
    1.13  text {* Operations on relations *}
    1.14