# HG changeset patch
# User nipkow
# Date 1521900433 -3600
# Node ID a3e5f08e6b589d93560646e6620a5002dfa59657
# Parent  49a34b2fa788b6803878aaead7d152f0e6bc6021
added lemma

diff -r 49a34b2fa788 -r a3e5f08e6b58 src/HOL/List.thy
--- 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)