# HG changeset patch
# User haftmann
# Date 1218459002 -7200
# Node ID 12254665fc41ad988d03653b6ccc493f12b1cf89
# Parent  97d2a3797ce0cb8b9826dc12a687fadc2815dc73
re-arranged class dense_linear_order

diff -r 97d2a3797ce0 -r 12254665fc41 src/HOL/Library/Dense_Linear_Order.thy
--- a/src/HOL/Library/Dense_Linear_Order.thy	Mon Aug 11 14:50:00 2008 +0200
+++ b/src/HOL/Library/Dense_Linear_Order.thy	Mon Aug 11 14:50:02 2008 +0200
@@ -214,6 +214,10 @@
 context dense_linear_order
 begin
 
+lemma interval_empty_iff:
+  "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
+  by (auto dest: dense)
+
 lemma dlo_qe_bnds: 
   assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
   shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l < u)"
diff -r 97d2a3797ce0 -r 12254665fc41 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Mon Aug 11 14:50:00 2008 +0200
+++ b/src/HOL/Real/PReal.thy	Mon Aug 11 14:50:02 2008 +0200
@@ -10,7 +10,7 @@
 header {* Positive real numbers *}
 
 theory PReal
-imports Rational
+imports Rational Dense_Linear_Order
 begin
 
 text{*Could be generalized and moved to @{text Ring_and_Field}*}