src/HOL/Log.thy

 by (simp add: powr_def)
 declare powr_one_gt_zero_iff [THEN iffD2, simp]
 
 lemma powr_mult: 
       "[| 0 < x; 0 < y |] ==> (x * y) powr a = (x powr a) * (y powr a)"
-by (simp add: powr_def exp_add [symmetric] ln_mult right_distrib)
+by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
 
 lemma powr_gt_zero [simp]: "0 < x powr a"
 by (simp add: powr_def)
 
 lemma powr_ge_pzero [simp]: "0 <= x powr y"

   apply (subst exp_diff [THEN sym])
   apply (simp add: left_diff_distrib)
 done
 
 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
-by (simp add: powr_def exp_add [symmetric] left_distrib)
+by (simp add: powr_def exp_add [symmetric] distrib_right)
 
 lemma powr_mult_base:
   "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
 using assms by (auto simp: powr_add)
 

 by (simp add: log_def powr_def)
 
 lemma log_mult: 
      "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]  
       ==> log a (x * y) = log a x + log a y"
-by (simp add: log_def ln_mult divide_inverse left_distrib)
+by (simp add: log_def ln_mult divide_inverse distrib_right)
 
 lemma log_eq_div_ln_mult_log: 
      "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
       ==> log a x = (ln b/ln a) * log b x"
 by (simp add: log_def divide_inverse)