| changeset 39728 | 832c42be723e |
| parent 39613 | 7723505c746a |
| child 39774 | 30cf9d80939e |
--- a/src/HOL/List.thy Mon Sep 27 14:13:22 2010 +0200 +++ b/src/HOL/List.thy Mon Sep 27 14:13:22 2010 +0200 @@ -2862,6 +2862,10 @@ with `distinct xs` show ?thesis by simp qed +lemma remdups_map_remdups: + "remdups (map f (remdups xs)) = remdups (map f xs)" + by (induct xs) simp_all + subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}