--- a/src/HOL/Real/RealBin.thy Mon Oct 04 21:46:49 1999 +0200
+++ b/src/HOL/Real/RealBin.thy Mon Oct 04 21:47:16 1999 +0200
@@ -8,7 +8,7 @@
This case is reduced to that for the integers
*)
-RealBin = RealInt + Bin +
+RealBin = RealInt + IntArith +
instance
real :: number