src/HOL/Real/RealOrd.thy

--- a/src/HOL/Real/RealOrd.thy	Mon May 08 18:20:04 2000 +0200
+++ b/src/HOL/Real/RealOrd.thy	Mon May 08 20:57:02 2000 +0200
@@ -11,8 +11,7 @@
 instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
 instance real :: linorder (real_le_linear)
 
-constdefs
-   rabs   :: real => real
-   "rabs r      == if 0r<=r then r else -r" 
+defs
+  abs_real_def "abs r == (if 0r <= r then r else -r)"
 
 end