--- a/src/HOL/Real/RComplete.thy Thu Aug 19 17:06:05 1999 +0200 +++ b/src/HOL/Real/RComplete.thy Thu Aug 19 18:36:41 1999 +0200 @@ -6,5 +6,5 @@ reals and reals *) -RComplete = Lubs + Real +RComplete = Lubs + RealBin