src/HOL/Power.thy
changeset 23305 8ae6f7b0903b
parent 23183 af27d3ad9baf
child 23431 25ca91279a9b
     1.1 --- a/src/HOL/Power.thy	Mon Jun 11 01:22:29 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Mon Jun 11 02:24:39 2007 +0200
     1.3 @@ -331,6 +331,10 @@
     1.4    show "z^(Suc n) = z * (z^n)" by simp
     1.5  qed
     1.6  
     1.7 +lemma of_nat_power:
     1.8 +  "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
     1.9 +by (induct n, simp_all add: power_Suc)
    1.10 +
    1.11  lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
    1.12  by (insert one_le_power [of i n], simp)
    1.13