--- a/src/HOL/Real/RealAbs.thy Mon Jul 24 23:59:08 2000 +0200 +++ b/src/HOL/Real/RealAbs.thy Mon Jul 24 23:59:32 2000 +0200 @@ -5,7 +5,7 @@ Description : Absolute value function for the reals *) -RealAbs = RealBin + +RealAbs = RealArith + defs