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.
added lemma
authornipkow
Sat, 24 Mar 2018 15:07:13 +0100
changeset 67942 a3e5f08e6b58
parent 67941 49a34b2fa788
child 67943 b45f0c0ea14f
added lemma
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.thy	Fri Mar 23 23:31:59 2018 +0100
+++ b/src/HOL/List.thy	Sat Mar 24 15:07:13 2018 +0100
@@ -3214,6 +3214,9 @@
 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
 by(simp add: upto.simps)
 
+lemma upto_single[simp]: "[i..i] = [i]"
+by(simp add: upto.simps)
+
 lemma upto_Nil[simp]: "[i..j] = [] \<longleftrightarrow> j < i"
 by (simp add: upto.simps)
isabelle