# HG changeset patch
# User nipkow
# Date 1414580499 -3600
# Node ID c04118553598eb83df7ef9170040bddf677101a1
# Parent  5b068376ff2027a768e8c03805ebb350a2091ce6
removed useless lemmas

diff -r 5b068376ff20 -r c04118553598 src/HOL/List.thy
--- 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="[]"])