src/HOL/Real/PReal.thy

--- a/src/HOL/Real/PReal.thy	Sat Feb 14 02:06:12 2004 +0100
+++ b/src/HOL/Real/PReal.thy	Sun Feb 15 10:46:37 2004 +0100
@@ -7,7 +7,7 @@
                   provides some of the definitions.
 *)
 
-theory PReal = RatArith:
+theory PReal = Rational:
 
 text{*Could be generalized and moved to @{text Ring_and_Field}*}
 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"