# HG changeset patch
# User mehta
# Date 1082123210 -7200
# Node ID 7be4d5dadf152f12a477163d7d95a78f5107cea3
# Parent  276ef51cedbf76104a758f7758f7f9ec0814b573
lemma drop_Suc_conv_tl added.

diff -r 276ef51cedbf -r 7be4d5dadf15 src/HOL/List.thy
--- 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)