--- a/src/HOL/Real/RealBin.thy Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/RealBin.thy Wed May 10 22:34:30 2000 +0200
@@ -8,7 +8,7 @@
This case is reduced to that for the integers
*)
-RealBin = RealInt + IntArith +
+RealBin = RealInt +
instance
real :: number