--- a/src/HOL/Decision_Procs/Approximation.thy Fri Aug 19 17:05:10 2011 +0900
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Aug 19 07:45:22 2011 -0700
@@ -959,7 +959,7 @@
hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
ultimately have even: "even n \<Longrightarrow> 0 \<le> ?rest" and odd: "odd n \<Longrightarrow> 0 \<le> - ?rest " by auto
- have "0 < ?fact" by (rule real_of_nat_fact_gt_zero)
+ have "0 < ?fact" by (simp del: fact_Suc)
have "0 < ?pow" using `0 < real x` by (rule zero_less_power)
{
--- a/src/HOL/Ln.thy Fri Aug 19 17:05:10 2011 +0900
+++ b/src/HOL/Ln.thy Fri Aug 19 07:45:22 2011 -0700
@@ -65,7 +65,7 @@
apply (rule mult_right_mono)
apply (subst inverse_eq_divide)
apply simp
- apply (rule inv_real_of_nat_fact_ge_zero)
+ apply (simp del: fact_Suc)
done
finally show ?thesis .
qed
--- a/src/HOL/Transcendental.thy Fri Aug 19 17:05:10 2011 +0900
+++ b/src/HOL/Transcendental.thy Fri Aug 19 07:45:22 2011 -0700
@@ -618,23 +618,6 @@
qed
-subsection{* Some properties of factorials *}
-
-lemma real_of_nat_fact_not_zero [simp]: "real (fact (n::nat)) \<noteq> 0"
-by auto
-
-lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact (n::nat))"
-by auto
-
-lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact (n::nat))"
-by simp
-
-lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact (n::nat)))"
-by (auto simp add: positive_imp_inverse_positive)
-
-lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact (n::nat)))"
-by (auto intro: order_less_imp_le)
-
subsection {* Derivability of power series *}
lemma DERIV_series': fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
@@ -1701,7 +1684,8 @@
apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
del: fact_Suc)
apply (rule real_mult_inverse_cancel2)
-apply (rule real_of_nat_fact_gt_zero)+
+apply (simp del: fact_Suc)
+apply (simp del: fact_Suc)
apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
apply (subst fact_lemma)
apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])