diff -r 06e195515deb -r 87429bdecad5 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Jun 30 15:45:21 2014 +0200
@@ -457,6 +457,15 @@
   shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
   using atLeastLessThan_inj assms by auto
 
+lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \<longleftrightarrow> (b \<le> a \<and> d \<le> c) \<or> a = c \<and> b = d"
+  by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le)
+
+lemma (in order) Iio_Int_singleton: "{..<k} \<inter> {x} = (if x < k then {x} else {})"
+  by auto
+
+lemma (in linorder) Ioc_subset_iff: "{a<..b} \<subseteq> {c<..d} \<longleftrightarrow> (b \<le> a \<or> c \<le> a \<and> b \<le> d)"
+  by (auto simp: subset_eq Ball_def) (metis less_le not_less)
+
 lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
 by (auto simp: set_eq_iff intro: le_bot)
 
@@ -588,6 +597,9 @@
 lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}"
   by (auto simp: min_def)
 
+lemma Ioc_disjoint: "{a<..b} \<inter> {c<..d} = {} \<longleftrightarrow> b \<le> a \<or> d \<le> c \<or> b \<le> c \<or> d \<le> a"
+  using assms by auto
+
 end
 
 context complete_lattice