diff -r efc5f4806cd5 -r c141f139ce26 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Jul 17 13:12:18 2009 -0400
@@ -2514,7 +2514,7 @@
 proof-
   {fix n
     have "?l$n = ?r $ n"
-  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc_nat of_nat_Suc power_Suc)
+  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
   by (simp add: of_nat_mult ring_simps)}
 then show ?thesis by (simp add: fps_eq_iff)
 qed
@@ -2531,7 +2531,7 @@
       apply simp
       unfolding th
       using fact_gt_zero_nat
-      apply (simp add: field_simps del: of_nat_Suc fact_Suc_nat)
+      apply (simp add: field_simps del: of_nat_Suc fact_Suc)
       apply (drule sym)
       by (simp add: ring_simps of_nat_mult power_Suc)}
   note th' = this
@@ -2697,7 +2697,7 @@
       also have "\<dots> = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))"
 	using en by (simp add: fps_sin_def)
       also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
-	unfolding fact_Suc_nat of_nat_mult
+	unfolding fact_Suc of_nat_mult
 	by (simp add: field_simps del: of_nat_add of_nat_Suc)
       also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
 	by (simp add: field_simps del: of_nat_add of_nat_Suc)
@@ -2721,7 +2721,7 @@
       also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))"
 	using en by (simp add: fps_cos_def)
       also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
-	unfolding fact_Suc_nat of_nat_mult
+	unfolding fact_Suc of_nat_mult
 	by (simp add: field_simps del: of_nat_add of_nat_Suc)
       also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
 	by (simp add: field_simps del: of_nat_add of_nat_Suc)
@@ -2763,7 +2763,7 @@
   "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))"
 unfolding fps_sin_def
 apply (cases n, simp)
-apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
+apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
 apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
 done
 
@@ -2776,7 +2776,7 @@
 lemma fps_cos_nth_add_2:
   "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"
 unfolding fps_cos_def
-apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
+apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
 apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
 done