# HG changeset patch
# User huffman
# Date 1313765122 25200
# Node ID 3bdc02eb16371de4405f6fab27fde4ed40c29e33
# Parent  83c4f8ba0aa328114a1bc0dd2b72a68bf838de33
remove some redundant simp rules

diff -r 83c4f8ba0aa3 -r 3bdc02eb1637 src/HOL/Decision_Procs/Approximation.thy
--- 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)
 
     {
diff -r 83c4f8ba0aa3 -r 3bdc02eb1637 src/HOL/Ln.thy
--- 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
diff -r 83c4f8ba0aa3 -r 3bdc02eb1637 src/HOL/Transcendental.thy
--- 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)))))))"])