--- a/src/HOL/Real/RealAbs.thy Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Real/RealAbs.thy Fri Nov 02 17:55:24 2001 +0100
@@ -9,6 +9,6 @@
defs
- real_abs_def "abs r == (if (Numeral0::real) <= r then r else -r)"
+ real_abs_def "abs r == (if (0::real) <= r then r else -r)"
end