--- a/src/HOL/Transcendental.thy Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Transcendental.thy Fri Jul 17 13:12:18 2009 -0400
@@ -1604,11 +1604,11 @@
apply (rotate_tac 2)
apply (drule sin_paired [THEN sums_unique, THEN ssubst])
unfolding One_nat_def
-apply (auto simp del: fact_Suc_nat)
+apply (auto simp del: fact_Suc)
apply (frule sums_unique)
-apply (auto simp del: fact_Suc_nat)
+apply (auto simp del: fact_Suc)
apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
-apply (auto simp del: fact_Suc_nat)
+apply (auto simp del: fact_Suc)
apply (erule sums_summable)
apply (case_tac "m=0")
apply (simp (no_asm_simp))
@@ -1617,24 +1617,24 @@
apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
apply (subgoal_tac "x*x < 2*3", simp)
apply (rule mult_strict_mono)
-apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc_nat)
-apply (subst fact_Suc_nat)
-apply (subst fact_Suc_nat)
-apply (subst fact_Suc_nat)
-apply (subst fact_Suc_nat)
+apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
+apply (subst fact_Suc)
+apply (subst fact_Suc)
+apply (subst fact_Suc)
+apply (subst fact_Suc)
apply (subst real_of_nat_mult)
apply (subst real_of_nat_mult)
apply (subst real_of_nat_mult)
apply (subst real_of_nat_mult)
-apply (simp (no_asm) add: divide_inverse del: fact_Suc_nat)
-apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc_nat)
+apply (simp (no_asm) add: divide_inverse del: fact_Suc)
+apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right)
-apply (auto simp add: mult_assoc simp del: fact_Suc_nat)
+apply (auto simp add: mult_assoc simp del: fact_Suc)
apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right)
-apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc_nat)
+apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)")
apply (erule ssubst)+
-apply (auto simp del: fact_Suc_nat)
+apply (auto simp del: fact_Suc)
apply (subgoal_tac "0 < x ^ (4 * m) ")
prefer 2 apply (simp only: zero_less_power)
apply (simp (no_asm_simp) add: mult_less_cancel_left)
@@ -1670,18 +1670,18 @@
apply (rule_tac y =
"\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
in order_less_trans)
-apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc_nat)
+apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc)
apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
apply (rule sumr_pos_lt_pair)
apply (erule sums_summable, safe)
unfolding One_nat_def
apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
- del: fact_Suc_nat)
+ del: fact_Suc)
apply (rule real_mult_inverse_cancel2)
apply (rule real_of_nat_fact_gt_zero)+
-apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc_nat)
+apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
apply (subst fact_lemma)
-apply (subst fact_Suc_nat [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
+apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
apply (simp only: real_of_nat_mult)
apply (rule mult_strict_mono, force)
apply (rule_tac [3] real_of_nat_ge_zero)