1.1 --- a/src/HOL/Power.thy	Mon Feb 23 13:55:36 2009 -0800
     1.2 +++ b/src/HOL/Power.thy	Mon Feb 23 16:25:52 2009 -0800
     1.3 @@ -31,7 +31,7 @@
     1.4    by (induct n) (simp_all add: power_Suc)
     1.5  
     1.6  lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
     1.7 -  by (simp add: power_Suc)
     1.8 +  unfolding One_nat_def by (simp add: power_Suc)
     1.9  
    1.10  lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
    1.11    by (induct n) (simp_all add: power_Suc mult_assoc)
    1.12 @@ -366,8 +366,8 @@
    1.13    "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
    1.14  by (induct n, simp_all add: power_Suc of_nat_mult)
    1.15  
    1.16 -lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
    1.17 -by (insert one_le_power [of i n], simp)
    1.18 +lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n"
    1.19 +by (rule one_le_power [of i n, unfolded One_nat_def])
    1.20  
    1.21  lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
    1.22  by (induct "n", auto)
    1.23 @@ -452,4 +452,3 @@
    1.24  *}
    1.25  
    1.26  end
    1.27 -