# HG changeset patch
# User haftmann
# Date 1285589602 -7200
# Node ID 832c42be723e09933bc884376c0bf73bc601eede
# Parent  5dab9549c80d068e27db21316a4157a6424bee54
lemma remdups_map_remdups

diff -r 5dab9549c80d -r 832c42be723e src/HOL/List.thy
--- 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>"}*}