1.1 --- a/src/HOL/Power.thy	Wed Jun 20 05:06:56 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Jun 20 05:18:39 2007 +0200
     1.3 @@ -333,7 +333,7 @@
     1.4  
     1.5  lemma of_nat_power:
     1.6    "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
     1.7 -by (induct n, simp_all add: power_Suc)
     1.8 +by (induct n, simp_all add: power_Suc of_nat_mult)
     1.9  
    1.10  lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
    1.11  by (insert one_le_power [of i n], simp)