--- a/src/HOL/Set_Interval.thy Tue May 13 11:11:51 2014 +0200
+++ b/src/HOL/Set_Interval.thy Tue May 13 11:35:47 2014 +0200
@@ -467,6 +467,12 @@
"{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)"
by (auto simp: set_eq_iff intro: top_le le_bot)
+lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \<longleftrightarrow> n = bot"
+ by (auto simp: set_eq_iff not_less le_bot)
+
+lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
+ by (simp add: Iio_eq_empty_iff bot_nat_def)
+
subsection {* Infinite intervals *}