# HG changeset patch
# User nipkow
# Date 1259911585 -3600
# Node ID 8493ed132fed5d3443d9b74c65e0fd0efb4ede91
# Parent  ab87cceed53fda6f7d56de6878a8a75f8e2f75fd
added remdups_filter lemma

diff -r ab87cceed53f -r 8493ed132fed src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 02 17:53:44 2009 +0100
+++ b/src/HOL/List.thy	Fri Dec 04 08:26:25 2009 +0100
@@ -2665,6 +2665,10 @@
 apply(rule length_remdups_leq)
 done
 
+lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
+apply(induct xs)
+apply auto
+done
 
 lemma distinct_map:
   "distinct(map f xs) = (distinct xs & inj_on f (set xs))"