# HG changeset patch
# User berghofe
# Date 1228224552 -3600
# Node ID da79ac67794b7d57893736da032d3645d9bf1924
# Parent  e27abf0db98478cde433a96eb1c9b31a3b1e8c43
Corrected imports.

diff -r e27abf0db984 -r da79ac67794b src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Mon Dec 01 15:36:48 2008 -0800
+++ b/src/HOL/Real/PReal.thy	Tue Dec 02 14:29:12 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title       : PReal.thy
-    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The positive reals as Dedekind sections of positive
@@ -10,7 +9,7 @@
 header {* Positive real numbers *}
 
 theory PReal
-imports Rational Dense_Linear_Order
+imports Rational "~~/src/HOL/Library/Dense_Linear_Order"
 begin
 
 text{*Could be generalized and moved to @{text Ring_and_Field}*}