src/HOL/Num.thy
changeset 61944 5d06ecfdb472
parent 61799 4cf66f21b764
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/Num.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/Num.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -954,14 +954,13 @@
     1.4    "\<not> 1 < - 1"
     1.5    by (simp_all add: less_le)
     1.6  
     1.7 -lemma abs_numeral [simp]: "abs (numeral n) = numeral n"
     1.8 +lemma abs_numeral [simp]: "\<bar>numeral n\<bar> = numeral n"
     1.9    by simp
    1.10  
    1.11 -lemma abs_neg_numeral [simp]: "abs (- numeral n) = numeral n"
    1.12 +lemma abs_neg_numeral [simp]: "\<bar>- numeral n\<bar> = numeral n"
    1.13    by (simp only: abs_minus_cancel abs_numeral)
    1.14  
    1.15 -lemma abs_neg_one [simp]:
    1.16 -  "abs (- 1) = 1"
    1.17 +lemma abs_neg_one [simp]: "\<bar>- 1\<bar> = 1"
    1.18    by simp
    1.19  
    1.20  end