# HG changeset patch
# User nipkow
# Date 1538754550 -7200
# Node ID 60b6c759134f7a658e47cef7be0a051e304756a8
# Parent  6ededdc829bb01f4f31bf6c353bb89d612259bc3
more [simp]

diff -r 6ededdc829bb -r 60b6c759134f src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Oct 04 16:40:03 2018 +0200
+++ b/src/HOL/List.thy	Fri Oct 05 17:49:10 2018 +0200
@@ -3232,7 +3232,7 @@
     unfolding upto.simps[of i j] by auto
 qed
 
-lemma nth_upto: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
+lemma nth_upto[simp]: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
   apply(induction i j arbitrary: k rule: upto.induct)
 apply(subst upto_rec1)
 apply(auto simp add: nth_Cons')