--- a/src/HOL/Real/RealAbs.thy Thu Dec 21 10:16:07 2000 +0100
+++ b/src/HOL/Real/RealAbs.thy Thu Dec 21 10:16:33 2000 +0100
@@ -9,6 +9,6 @@
defs
- abs_real_def "abs r == (if (#0::real) <= r then r else -r)"
+ real_abs_def "abs r == (if (#0::real) <= r then r else -r)"
end