| changeset 61945 | 1135b8de26c3 |
| parent 61605 | 1bf7b186542e |
| child 62065 | 1546a042e87b |
--- a/src/HOL/Library/Polynomial.thy Mon Dec 28 01:26:34 2015 +0100 +++ b/src/HOL/Library/Polynomial.thy Mon Dec 28 01:28:28 2015 +0100 @@ -1062,7 +1062,7 @@ "x \<le> y \<longleftrightarrow> x = y \<or> pos_poly (y - x)" definition - "abs (x::'a poly) = (if x < 0 then - x else x)" + "\<bar>x::'a poly\<bar> = (if x < 0 then - x else x)" definition "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"