--- a/src/HOL/Power.thy Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/Power.thy Fri Feb 28 17:54:52 2014 +0100
@@ -613,7 +613,7 @@
lemma self_le_power:
fixes x::"'a::linordered_semidom"
shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n"
- by (metis gr_implies_not0 le_eq_less_or_eq less_one nat_le_linear power_increasing power_one_right)
+ using power_increasing[of 1 n x] power_one_right[of x] by auto
lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
unfolding One_nat_def by (cases m) simp_all