src/HOL/Power.thy
changeset 54489 03ff4d1e6784
parent 54249 ce00f2fef556
child 55096 916b2ac758f4
     1.1 --- a/src/HOL/Power.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Power.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -209,14 +209,6 @@
     1.4    "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
     1.5    by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left)
     1.6  
     1.7 -lemma power_neg_numeral_Bit0 [simp]:
     1.8 -  "neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))"
     1.9 -  by (simp only: neg_numeral_def power_minus_Bit0 power_numeral)
    1.10 -
    1.11 -lemma power_neg_numeral_Bit1 [simp]:
    1.12 -  "neg_numeral k ^ numeral (Num.Bit1 l) = neg_numeral (Num.pow k (Num.Bit1 l))"
    1.13 -  by (simp only: neg_numeral_def power_minus_Bit1 power_numeral pow.simps)
    1.14 -
    1.15  lemma power2_minus [simp]:
    1.16    "(- a)\<^sup>2 = a\<^sup>2"
    1.17    by (rule power_minus_Bit0)