--- a/src/HOL/Real/Real.thy Tue Sep 21 17:28:33 1999 +0200 +++ b/src/HOL/Real/Real.thy Tue Sep 21 17:29:00 1999 +0200 @@ -1,2 +1,2 @@ -Real = RComplete +Real = Main + RComplete