--- a/src/HOL/Real/RComplete.thy Mon Jul 24 23:59:08 2000 +0200 +++ b/src/HOL/Real/RComplete.thy Mon Jul 24 23:59:32 2000 +0200 @@ -6,5 +6,5 @@ reals and reals *) -RComplete = Lubs + RealBin +RComplete = Lubs + RealArith