| author | haftmann |
| Mon, 27 Sep 2010 14:13:22 +0200 | |
| changeset 39728 | 832c42be723e |
| parent 39727 | 5dab9549c80d |
| child 39729 | 6a64f04cb648 |
| child 39743 | 7aef0e4a3aac |
| src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- 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>"}*}