diff -r ee8572f3bb57 -r 6d4cb27ed19c 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}*}