lemma drop_Suc_conv_tl added.

--- a/src/HOL/List.thy	Fri Apr 16 13:52:43 2004 +0200
+++ b/src/HOL/List.thy	Fri Apr 16 15:46:50 2004 +0200
@@ -847,6 +847,12 @@
 apply (case_tac i, auto)
 done
 
+lemma drop_Suc_conv_tl:
+  "!!i. i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
+apply (induct xs, simp)
+apply (case_tac i, auto)
+done
+
 lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n"
 by (induct n) (auto, case_tac xs, auto)