more [simp]
authornipkow
Fri Oct 05 17:49:10 2018 +0200 (10 months ago)
changeset 6912560b6c759134f
parent 69124 6ededdc829bb
child 69126 e1b4b14ded58
more [simp]
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Thu Oct 04 16:40:03 2018 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Oct 05 17:49:10 2018 +0200
     1.3 @@ -3232,7 +3232,7 @@
     1.4      unfolding upto.simps[of i j] by auto
     1.5  qed
     1.6  
     1.7 -lemma nth_upto: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
     1.8 +lemma nth_upto[simp]: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
     1.9    apply(induction i j arbitrary: k rule: upto.induct)
    1.10  apply(subst upto_rec1)
    1.11  apply(auto simp add: nth_Cons')