src/HOL/List.thy

--- a/src/HOL/List.thy	Wed May 12 22:33:10 2010 -0700
+++ b/src/HOL/List.thy	Thu May 13 14:34:05 2010 +0200
@@ -2961,6 +2961,9 @@
   (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
 by (induct xs) auto
 
+lemma remove1_commute: "remove1 x (remove1 y zs) = remove1 y (remove1 x zs)"
+by (induct zs) auto
+
 lemma in_set_remove1[simp]:
   "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
 apply (induct xs)