src/HOL/Ln.thy
changeset 44305 3bdc02eb1637
parent 44289 d81d09cdab9c
child 47242 1caeecc72aea
--- a/src/HOL/Ln.thy	Fri Aug 19 17:05:10 2011 +0900
+++ b/src/HOL/Ln.thy	Fri Aug 19 07:45:22 2011 -0700
@@ -65,7 +65,7 @@
         apply (rule mult_right_mono)
         apply (subst inverse_eq_divide)
         apply simp
-        apply (rule inv_real_of_nat_fact_ge_zero)
+        apply (simp del: fact_Suc)
         done
       finally show ?thesis .
     qed