1.1 --- a/src/HOL/Ln.thy	Fri Aug 19 17:05:10 2011 +0900
     1.2 +++ b/src/HOL/Ln.thy	Fri Aug 19 07:45:22 2011 -0700
     1.3 @@ -65,7 +65,7 @@
     1.4          apply (rule mult_right_mono)
     1.5          apply (subst inverse_eq_divide)
     1.6          apply simp
     1.7 -        apply (rule inv_real_of_nat_fact_ge_zero)
     1.8 +        apply (simp del: fact_Suc)
     1.9          done
    1.10        finally show ?thesis .
    1.11      qed