diff -r dc6be28d7f4e -r c69542757a4d src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Real/PReal.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -7,7 +7,9 @@
                   provides some of the definitions.
 *)
 
-theory PReal = Rational:
+theory PReal
+import Rational
+begin
 
 text{*Could be generalized and moved to @{text Ring_and_Field}*}
 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"