src/HOL/Power.thy
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)