src/HOL/Log.thy

--- a/src/HOL/Log.thy	Wed Apr 18 14:29:17 2012 +0200
+++ b/src/HOL/Log.thy	Wed Apr 18 14:29:18 2012 +0200
@@ -285,6 +285,10 @@
   apply (rule powr_less_mono2, auto)
 done
 
+lemma powr_inj:
+  "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
+  unfolding powr_def exp_inj_iff by simp
+
 lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
   apply (rule mult_imp_le_div_pos)
   apply (assumption)