src/HOL/PReal.thy

--- a/src/HOL/PReal.thy	Mon Dec 29 13:23:53 2008 +0100
+++ b/src/HOL/PReal.thy	Mon Dec 29 14:08:08 2008 +0100
@@ -9,7 +9,7 @@
 header {* Positive real numbers *}
 
 theory PReal
-imports Rational "~~/src/HOL/Library/Dense_Linear_Order"
+imports Rational Dense_Linear_Order
 begin
 
 text{*Could be generalized and moved to @{text Ring_and_Field}*}