| changeset 61944 | 5d06ecfdb472 |
| parent 61942 | f02b26f7d39d |
| child 62079 | 3a21fddf0328 |
--- a/src/HOL/Rat.thy Sun Dec 27 22:07:17 2015 +0100 +++ b/src/HOL/Rat.thy Mon Dec 28 01:26:34 2015 +0100 @@ -451,7 +451,7 @@ "x \<le> (y::rat) \<longleftrightarrow> x < y \<or> x = y" definition - "abs (a::rat) = (if a < 0 then - a else a)" + "\<bar>a::rat\<bar> = (if a < 0 then - a else a)" definition "sgn (a::rat) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"