--- a/src/HOL/Real/PReal.thy Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Real/PReal.thy Wed Aug 18 11:09:40 2004 +0200
@@ -8,7 +8,7 @@
*)
theory PReal
-import Rational
+imports Rational
begin
text{*Could be generalized and moved to @{text Ring_and_Field}*}