# HG changeset patch
# User hoelzl
# Date 1283415495 -7200
# Node ID 8520a1f89db12ae8d35dda82038e9e7db6c9aa76
# Parent  1030b1a166efb0380630fd1afab8e37e5c4c8671
Add filter_remove1

diff -r 1030b1a166ef -r 8520a1f89db1 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 02 10:14:32 2010 +0200
+++ b/src/HOL/List.thy	Thu Sep 02 10:18:15 2010 +0200
@@ -3076,6 +3076,10 @@
   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
 by(induct xs) auto
 
+lemma filter_remove1:
+  "filter Q (remove1 x xs) = remove1 x (filter Q xs)"
+by (induct xs) auto
+
 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
 apply(insert set_remove1_subset)
 apply fast