added lemma
authornipkow
Sat Mar 24 15:07:13 2018 +0100 (14 months ago)
changeset 67942a3e5f08e6b58
parent 67941 49a34b2fa788
child 67943 b45f0c0ea14f
added lemma
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Fri Mar 23 23:31:59 2018 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Mar 24 15:07:13 2018 +0100
     1.3 @@ -3214,6 +3214,9 @@
     1.4  lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
     1.5  by(simp add: upto.simps)
     1.6  
     1.7 +lemma upto_single[simp]: "[i..i] = [i]"
     1.8 +by(simp add: upto.simps)
     1.9 +
    1.10  lemma upto_Nil[simp]: "[i..j] = [] \<longleftrightarrow> j < i"
    1.11  by (simp add: upto.simps)
    1.12