src/HOL/Real/RealAbs.thy

--- a/src/HOL/Real/RealAbs.thy	Wed May 31 18:06:02 2000 +0200
+++ b/src/HOL/Real/RealAbs.thy	Thu Jun 01 11:22:27 2000 +0200
@@ -7,4 +7,8 @@
 
 RealAbs = RealBin +
 
+
+defs
+  abs_real_def "abs r == (if (#0::real) <= r then r else -r)"
+
 end