diff -r f69045fdc836 -r d8f76db6a207 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 25 08:46:52 2011 +0100
+++ b/src/HOL/List.thy	Fri Feb 25 14:25:41 2011 +0100
@@ -1321,6 +1321,9 @@
 
 declare nth.simps [simp del]
 
+lemma nth_Cons_pos[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
+by(auto simp: Nat.gr0_conv_Suc)
+
 lemma nth_append:
   "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
 apply (induct xs arbitrary: n, simp)