changeset 23431 | 25ca91279a9b |
parent 23305 | 8ae6f7b0903b |
child 23544 | 4b4165cb3e0d |
--- a/src/HOL/Power.thy Wed Jun 20 05:06:56 2007 +0200 +++ b/src/HOL/Power.thy Wed Jun 20 05:18:39 2007 +0200 @@ -333,7 +333,7 @@ lemma of_nat_power: "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n" -by (induct n, simp_all add: power_Suc) +by (induct n, simp_all add: power_Suc of_nat_mult) lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n" by (insert one_le_power [of i n], simp)