--- a/src/HOL/Real/Real.thy Sun Jan 13 19:42:30 2002 +0100 +++ b/src/HOL/Real/Real.thy Sun Jan 13 19:45:17 2002 +0100 @@ -1,2 +1,2 @@ -Real = RComplete + RealPow +Real = RComplete + Complex_Numbers