# HG changeset patch
# User bulwahn
# Date 1328020785 -3600
# Node ID 26c422552cfe118d7ee658ca436582403d34ce04
# Parent  b99ca1a7c63ba472e117ce7d344564c7e7e6f6c7
adding code equation for setsum

diff -r b99ca1a7c63b -r 26c422552cfe src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jan 31 15:13:18 2012 +0100
+++ b/src/HOL/List.thy	Tue Jan 31 15:39:45 2012 +0100
@@ -5674,6 +5674,11 @@
   "Pow (set (x # xs)) = (let A = Pow (set xs) in A \<union> insert x ` A)"
   by (simp_all add: Pow_insert Let_def)
 
+text {* Further operations on sets *}
+
+lemma setsum_code [code]:
+  "setsum f (set xs) = listsum (map f (remdups xs))"
+by (simp add: listsum_distinct_conv_setsum_set)
 
 text {* Operations on relations *}