1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 19 17:05:10 2011 +0900
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 19 07:45:22 2011 -0700
     1.3 @@ -959,7 +959,7 @@
     1.4      hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
     1.5      ultimately have even: "even n \<Longrightarrow> 0 \<le> ?rest" and odd: "odd n \<Longrightarrow> 0 \<le> - ?rest " by auto
     1.6  
     1.7 -    have "0 < ?fact" by (rule real_of_nat_fact_gt_zero)
     1.8 +    have "0 < ?fact" by (simp del: fact_Suc)
     1.9      have "0 < ?pow" using `0 < real x` by (rule zero_less_power)
    1.10  
    1.11      {

     2.1 --- a/src/HOL/Ln.thy	Fri Aug 19 17:05:10 2011 +0900
     2.2 +++ b/src/HOL/Ln.thy	Fri Aug 19 07:45:22 2011 -0700
     2.3 @@ -65,7 +65,7 @@
     2.4          apply (rule mult_right_mono)
     2.5          apply (subst inverse_eq_divide)
     2.6          apply simp
     2.7 -        apply (rule inv_real_of_nat_fact_ge_zero)
     2.8 +        apply (simp del: fact_Suc)
     2.9          done
    2.10        finally show ?thesis .
    2.11      qed

     3.1 --- a/src/HOL/Transcendental.thy	Fri Aug 19 17:05:10 2011 +0900
     3.2 +++ b/src/HOL/Transcendental.thy	Fri Aug 19 07:45:22 2011 -0700
     3.3 @@ -618,23 +618,6 @@
     3.4  qed
     3.5  
     3.6  
     3.7 -subsection{* Some properties of factorials *}
     3.8 -
     3.9 -lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0"
    3.10 -by auto
    3.11 -
    3.12 -lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))"
    3.13 -by auto
    3.14 -
    3.15 -lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))"
    3.16 -by simp
    3.17 -
    3.18 -lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))"
    3.19 -by (auto simp add: positive_imp_inverse_positive)
    3.20 -
    3.21 -lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))"
    3.22 -by (auto intro: order_less_imp_le)
    3.23 -
    3.24  subsection {* Derivability of power series *}
    3.25  
    3.26  lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
    3.27 @@ -1701,7 +1684,8 @@
    3.28  apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
    3.29              del: fact_Suc)
    3.30  apply (rule real_mult_inverse_cancel2)
    3.31 -apply (rule real_of_nat_fact_gt_zero)+
    3.32 +apply (simp del: fact_Suc)
    3.33 +apply (simp del: fact_Suc)
    3.34  apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
    3.35  apply (subst fact_lemma)
    3.36  apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])