src/HOL/List.thy

--- a/src/HOL/List.thy	Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/List.thy	Thu Jun 16 17:57:09 2016 +0200
@@ -3039,6 +3039,9 @@
 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
 by(simp add:upt_conv_Cons)
 
+lemma tl_upt: "tl [m..<n] = [Suc m..<n]"
+  by (simp add: upt_rec)
+
 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
 by(cases j)(auto simp: upt_Suc_append)