--- a/src/HOL/Real/Real.thy Mon Jul 24 23:59:46 2000 +0200 +++ b/src/HOL/Real/Real.thy Tue Jul 25 00:00:03 2000 +0200 @@ -1,2 +1,2 @@ -Real = Main + RComplete + RealPow +Real = RComplete + RealPow