author | bulwahn |
Tue, 31 Jan 2012 15:39:45 +0100 | |
changeset 46383 | 26c422552cfe |
parent 46382 | b99ca1a7c63b |
child 46384 | 90be435411f0 |
src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- 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 *}