| changeset 33972 | daf65be6bfe5 |
| parent 33945 | 8493ed132fed |
| parent 33968 | f94fb13ecbb3 |
| child 34007 | aea892559fc5 |
--- a/src/HOL/List.thy Fri Dec 04 12:17:43 2009 +0100 +++ b/src/HOL/List.thy Fri Dec 04 12:22:09 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))"