changeset 39073 | 8520a1f89db1 |
parent 38857 | 97775f3e8722 |
child 39198 | f967a16dfcdd |
--- 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