--- a/src/HOL/Set_Interval.thy Thu Jan 31 11:31:22 2013 +0100
+++ b/src/HOL/Set_Interval.thy Thu Jan 31 11:31:27 2013 +0100
@@ -117,6 +117,11 @@
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
by (blast intro: order_antisym)
+lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \<inter> { b <..} = { max a b <..}"
+ by auto
+
+lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \<inter> {..< b} = {..< min a b}"
+ by auto
subsection {* Logical Equivalences for Set Inclusion and Equality *}
@@ -190,6 +195,9 @@
breaks many proofs. Since it only helps blast, it is better to leave well
alone *}
+lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
+ by auto
+
end
subsubsection{* Emptyness, singletons, subset *}