src/HOL/Power.thy
changeset 47220 52426c62b5d0
parent 47209 4893907fe872
child 47241 243b33052e34
     1.1 --- a/src/HOL/Power.thy	Fri Mar 30 12:02:23 2012 +0200
     1.2 +++ b/src/HOL/Power.thy	Fri Mar 30 12:32:35 2012 +0200
     1.3 @@ -185,7 +185,7 @@
     1.4  
     1.5  lemma power_minus_Bit1:
     1.6    "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
     1.7 -  by (simp only: nat_number(4) power_Suc power_minus_Bit0 mult_minus_left)
     1.8 +  by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left)
     1.9  
    1.10  lemma power_neg_numeral_Bit0 [simp]:
    1.11    "neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))"