changeset 27483 | 7c58324cd418 |
parent 25875 | 536dfdc25e0a |
--- a/src/HOL/Hyperreal/Ln.thy Thu Jul 03 20:15:06 2008 +0200 +++ b/src/HOL/Hyperreal/Ln.thy Thu Jul 03 20:53:44 2008 +0200 @@ -85,7 +85,7 @@ apply (rule mult_nonneg_nonneg) apply simp apply (subst inverse_nonnegative_iff_nonnegative) - apply (rule real_of_nat_fact_ge_zero) + apply (rule real_of_nat_ge_zero) apply (rule zero_le_power) apply (rule a) done