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