--- a/src/HOL/List.thy Wed Oct 29 11:03:23 2014 +0100
+++ b/src/HOL/List.thy Wed Oct 29 12:01:39 2014 +0100
@@ -1954,12 +1954,6 @@
declare take_Cons [simp del] and drop_Cons [simp del]
-lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"
-by simp
-
-lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"
-by simp
-
lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
by(clarsimp simp add:neq_Nil_conv)
@@ -2298,9 +2292,6 @@
thus ?thesis using all `\<not> ?thesis` nth_length_takeWhile[of P xs] by auto
qed
-text{* The following two lemmmas could be generalized to an arbitrary
-property. *}
-
lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
by(induct xs) (auto simp: takeWhile_tail[where l="[]"])