src/HOL/Power.thy
changeset 47209 4893907fe872
parent 47192 0c0501cb6da6
child 47220 52426c62b5d0
     1.1 --- a/src/HOL/Power.thy	Fri Mar 30 08:11:52 2012 +0200
     1.2 +++ b/src/HOL/Power.thy	Fri Mar 30 09:08:29 2012 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4    by (induct n) (simp_all add: of_nat_mult)
     1.5  
     1.6  lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0"
     1.7 -  by (cases "numeral k :: nat", simp_all)
     1.8 +  by (simp add: numeral_eq_Suc)
     1.9  
    1.10  lemma zero_power2: "0\<twosuperior> = 0" (* delete? *)
    1.11    by (rule power_zero_numeral)