--- a/Closures.thy	Mon Sep 05 14:15:32 2011 +0000
+++ b/Closures.thy	Mon Sep 05 15:42:29 2011 +0000
@@ -253,17 +253,6 @@
 definition
   "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)"
 
-lemma [simp]:
-  assumes "i \<noteq> j" "a \<noteq> b"
-  shows "length_test ((a ^^^ i) @ (b ^^^ j)) a b \<noteq> length_test ((a ^^^ n) @ (b ^^^ n)) a b"
-using assms unfolding length_test_def by auto
-
-lemma [simp]:
-  assumes "a \<noteq> b"
-  shows "filter (op= a) ((a ^^^ i) @ (b ^^^ j)) = a ^^^ i"
-  and   "filter (op= b) ((a ^^^ i) @ (b ^^^ j)) = b ^^^ j"
-using assms by simp_all
-
 lemma length_test:
   "x = y \<Longrightarrow> length_test x a b = length_test y a b"
 by simp