src/HOL/Power.thy
changeset 30079 293b896b9c25
parent 30056 0a35bee25c20
child 30242 aea5d7fa7ef5
--- a/src/HOL/Power.thy	Mon Feb 23 13:55:36 2009 -0800
+++ b/src/HOL/Power.thy	Mon Feb 23 16:25:52 2009 -0800
@@ -31,7 +31,7 @@
   by (induct n) (simp_all add: power_Suc)
 
 lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
-  by (simp add: power_Suc)
+  unfolding One_nat_def by (simp add: power_Suc)
 
 lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
   by (induct n) (simp_all add: power_Suc mult_assoc)
@@ -366,8 +366,8 @@
   "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
 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)
+lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n"
+by (rule one_le_power [of i n, unfolded One_nat_def])
 
 lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
 by (induct "n", auto)
@@ -452,4 +452,3 @@
 *}
 
 end
-