1.1 --- a/src/HOL/Transcendental.thy	Fri Aug 19 17:05:10 2011 +0900
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Aug 19 07:45:22 2011 -0700
     1.3 @@ -618,23 +618,6 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -subsection{* Some properties of factorials *}
     1.8 -
     1.9 -lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0"
    1.10 -by auto
    1.11 -
    1.12 -lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))"
    1.13 -by auto
    1.14 -
    1.15 -lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))"
    1.16 -by simp
    1.17 -
    1.18 -lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))"
    1.19 -by (auto simp add: positive_imp_inverse_positive)
    1.20 -
    1.21 -lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))"
    1.22 -by (auto intro: order_less_imp_le)
    1.23 -
    1.24  subsection {* Derivability of power series *}
    1.25  
    1.26  lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
    1.27 @@ -1701,7 +1684,8 @@
    1.28  apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
    1.29              del: fact_Suc)
    1.30  apply (rule real_mult_inverse_cancel2)
    1.31 -apply (rule real_of_nat_fact_gt_zero)+
    1.32 +apply (simp del: fact_Suc)
    1.33 +apply (simp del: fact_Suc)
    1.34  apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
    1.35  apply (subst fact_lemma)
    1.36  apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])