Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more [simp]
authornipkow
Fri, 05 Oct 2018 17:49:10 +0200
changeset 69125 60b6c759134f
parent 69124 6ededdc829bb
child 69126 e1b4b14ded58
more [simp]
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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')
isabelle