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