--- a/src/HOL/Transcendental.thy Tue Nov 15 17:39:40 2016 +0100
+++ b/src/HOL/Transcendental.thy Tue Nov 22 16:22:05 2016 +0100
@@ -2634,6 +2634,10 @@
and less_powr_iff = log_less_iff[symmetric]
and le_powr_iff = log_le_iff[symmetric]
+lemma gr_one_powr[simp]:
+ fixes x y :: real shows "\<lbrakk> x > 1; y > 0 \<rbrakk> \<Longrightarrow> 1 < x powr y"
+by(simp add: less_powr_iff)
+
lemma floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
@@ -2712,6 +2716,7 @@
lemma log_powr: "x \<noteq> 0 \<Longrightarrow> log b (x powr y) = y * log b x"
by (simp add: log_def ln_powr)
+(* [simp] is not worth it, interferes with some proofs *)
lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
by (simp add: log_powr powr_realpow [symmetric])