src/HOL/Ln.thy
changeset 36777 be5461582d0f
parent 33667 958dc9f03611
child 40864 4abaaadfdaf2
     1.1 --- a/src/HOL/Ln.thy	Sun May 09 14:21:44 2010 -0700
     1.2 +++ b/src/HOL/Ln.thy	Sun May 09 17:47:43 2010 -0700
     1.3 @@ -206,7 +206,7 @@
     1.4      apply auto
     1.5      done
     1.6    also have "... = exp (-x)"
     1.7 -    by (auto simp add: exp_minus real_divide_def)
     1.8 +    by (auto simp add: exp_minus divide_inverse)
     1.9    finally have "1 - x <= exp (- x)" .
    1.10    also have "1 - x = exp (ln (1 - x))"
    1.11    proof -