# HG changeset patch
# User nipkow
# Date 870425959 -7200
# Node ID 5b2dcdc1829c974fc150471b2932d249a93cc6aa
# Parent  8f9ee0f79d9ad4b191900ee47f55b0802de43c0f
Generalized nth_drop (Conny).

diff -r 8f9ee0f79d9a -r 5b2dcdc1829c src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Aug 01 09:42:19 1997 +0200
+++ b/src/HOL/List.ML	Fri Aug 01 10:59:19 1997 +0200
@@ -558,7 +558,7 @@
 qed_spec_mp "nth_take";
 Addsimps [nth_take];
 
-goal thy  "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
+goal thy  "!xs i. n + i <= length xs --> nth i (drop n xs) = nth (n + i) xs";
 by (nat_ind_tac "n" 1);
  by (ALLGOALS Asm_simp_tac);
 by (rtac allI 1);