src/HOL/Ln.thy
changeset 33667 958dc9f03611
parent 32038 4127b89f48ab
child 36777 be5461582d0f
     1.1 --- a/src/HOL/Ln.thy	Fri Nov 13 11:34:05 2009 +0000
     1.2 +++ b/src/HOL/Ln.thy	Fri Nov 13 17:15:12 2009 +0000
     1.3 @@ -342,9 +342,6 @@
     1.4    apply auto
     1.5  done
     1.6  
     1.7 -lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
     1.8 -  by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
     1.9 -
    1.10  lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
    1.11  proof -
    1.12    assume "exp 1 <= x" and "x <= y"