src/HOL/Log.thy
changeset 49962 a8cc904a6820
parent 47595 836b4c4d7c86
child 50247 491c5c81c2e8
     1.1 --- a/src/HOL/Log.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Log.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  
     1.5  lemma powr_mult: 
     1.6        "[| 0 < x; 0 < y |] ==> (x * y) powr a = (x powr a) * (y powr a)"
     1.7 -by (simp add: powr_def exp_add [symmetric] ln_mult right_distrib)
     1.8 +by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
     1.9  
    1.10  lemma powr_gt_zero [simp]: "0 < x powr a"
    1.11  by (simp add: powr_def)
    1.12 @@ -58,7 +58,7 @@
    1.13  done
    1.14  
    1.15  lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
    1.16 -by (simp add: powr_def exp_add [symmetric] left_distrib)
    1.17 +by (simp add: powr_def exp_add [symmetric] distrib_right)
    1.18  
    1.19  lemma powr_mult_base:
    1.20    "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
    1.21 @@ -112,7 +112,7 @@
    1.22  lemma log_mult: 
    1.23       "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]  
    1.24        ==> log a (x * y) = log a x + log a y"
    1.25 -by (simp add: log_def ln_mult divide_inverse left_distrib)
    1.26 +by (simp add: log_def ln_mult divide_inverse distrib_right)
    1.27  
    1.28  lemma log_eq_div_ln_mult_log: 
    1.29       "[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]