# HG changeset patch
# User nipkow
# Date 1507779478 -7200
# Node ID e8282131ddf97079865d30fcdb42fbd98c4bc939
# Parent  c04f46a6f29d7222a8d336fa5d2643f39c10ae50
relaxed assm

diff -r c04f46a6f29d -r e8282131ddf9 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Oct 11 21:41:11 2017 +0200
+++ b/src/HOL/List.thy	Thu Oct 12 05:37:58 2017 +0200
@@ -1713,9 +1713,8 @@
 apply (case_tac n, auto)
 done
 
-lemma nth_tl:
-  assumes "n < length (tl x)" shows "tl x ! n = x ! Suc n"
-using assms by (induct x) auto
+lemma nth_tl: "n < length (tl xs) \<Longrightarrow> tl xs ! n = xs ! Suc n"
+by (induction xs) auto
 
 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
 by(cases xs) simp_all
@@ -2153,7 +2152,7 @@
 done
 
 lemma nth_drop [simp]:
-  "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
+  "n <= length xs ==> (drop n xs)!i = xs!(n + i)"
 apply (induct n arbitrary: xs i, auto)
  apply (case_tac xs, auto)
 done