src/HOL/NthRoot.thy
changeset 61944 5d06ecfdb472
parent 61649 268d88ec9087
child 61969 e01015e49041
     1.1 --- a/src/HOL/NthRoot.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/NthRoot.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  imports Deriv Binomial
     1.5  begin
     1.6  
     1.7 -lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"
     1.8 +lemma abs_sgn_eq: "\<bar>sgn x :: real\<bar> = (if x = 0 then 0 else 1)"
     1.9    by (simp add: sgn_real_def)
    1.10  
    1.11  lemma inverse_sgn: "sgn (inverse a) = inverse (sgn a :: real)"