# HG changeset patch
# User huffman
# Date 1179497473 -7200
# Node ID e025695d9b0e5ca27335699f926fc3da26a989e0
# Parent  c46abff9a7a081fbbf246e16b9f4810aeec59e19
use mult_strict_mono instead of real_mult_less_mono

diff -r c46abff9a7a0 -r e025695d9b0e src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Fri May 18 11:12:03 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri May 18 16:11:13 2007 +0200
@@ -1261,8 +1261,8 @@
 apply (subst fact_lemma) 
 apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
 apply (simp only: real_of_nat_mult)
-apply (rule real_mult_less_mono, force)
-  apply (rule_tac [3] real_of_nat_fact_gt_zero)
+apply (rule mult_strict_mono, force)
+  apply (rule_tac [3] real_of_nat_fact_ge_zero)
  prefer 2 apply force
 apply (rule real_of_nat_less_iff [THEN iffD2])
 apply (rule fact_less_mono, auto)