| changeset 67942 | a3e5f08e6b58 |
| parent 67717 | 5a1b299fe4af |
| child 67949 | 4bb49ed64933 |
--- 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)