# HG changeset patch
# User huffman
# Date 1215111224 -7200
# Node ID 7c58324cd418f7e759f45572540ae5c2379673fb
# Parent  c686f9abc99c40ca69e9ec4ef1b0a65d9b11a1cc
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero

diff -r c686f9abc99c -r 7c58324cd418 src/HOL/Hyperreal/Ln.thy
--- 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
diff -r c686f9abc99c -r 7c58324cd418 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Thu Jul 03 20:15:06 2008 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Thu Jul 03 20:53:44 2008 +0200
@@ -1344,7 +1344,7 @@
 apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
 apply (simp only: real_of_nat_mult)
 apply (rule mult_strict_mono, force)
-  apply (rule_tac [3] real_of_nat_fact_ge_zero)
+  apply (rule_tac [3] real_of_nat_ge_zero)
  prefer 2 apply force
 apply (rule real_of_nat_less_iff [THEN iffD2])
 apply (rule fact_less_mono, auto)