Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
authorhuffman
Thu, 03 Jul 2008 20:53:44 +0200
changeset 27483 7c58324cd418
parent 27482 c686f9abc99c
child 27484 dbb9981c3d18
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
src/HOL/Hyperreal/Ln.thy file | annotate | diff | comparison | revisions
src/HOL/Hyperreal/Transcendental.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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)
isabelle