# HG changeset patch
# User nipkow
# Date 1128000694 -7200
# Node ID 2e75155c5ed5bf2326020d3f305066b2c9622a7a
# Parent  9dab1e491d105fe99a94ab89c5d1b5ad561b467c
Added a few lemmas

diff -r 9dab1e491d10 -r 2e75155c5ed5 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Thu Sep 29 12:45:16 2005 +0200
+++ b/src/HOL/SetInterval.thy	Thu Sep 29 15:31:34 2005 +0200
@@ -196,8 +196,14 @@
 lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n::'a::order} = {}"
 by (auto simp add: atLeastLessThan_def)
 
+lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..(l::'a::order)} = {}"
+by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
+
+lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..(l::'a::order)} = {}"
+by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
+
 lemma atLeastAtMost_singleton [simp]: "{a::'a::order..a} = {a}";
-  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);
+by (auto simp add: atLeastAtMost_def atMost_def atLeast_def);
 
 subsection {* Intervals of natural numbers *}