| changeset 61945 | 1135b8de26c3 |
| parent 61933 | cf58b5b794b2 |
| child 67443 | 3abf6a722518 |
--- a/src/HOL/ex/Dedekind_Real.thy Mon Dec 28 01:26:34 2015 +0100 +++ b/src/HOL/ex/Dedekind_Real.thy Mon Dec 28 01:28:28 2015 +0100 @@ -1231,7 +1231,7 @@ real_less_def: "x < (y::real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y" definition - real_abs_def: "abs (r::real) = (if r < 0 then - r else r)" + real_abs_def: "\<bar>r::real\<bar> = (if r < 0 then - r else r)" definition real_sgn_def: "sgn (x::real) = (if x=0 then 0 else if 0<x then 1 else - 1)"