1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Fri Feb 18 11:48:42 2005 +0100
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Fri Feb 18 11:48:53 2005 +0100
     1.3 @@ -267,7 +267,7 @@
     1.4  apply (rule_tac x = "-t" in exI, auto)
     1.5  apply (subgoal_tac "(\<Sum>m = 0..<n. -1 ^ m * diff m 0 * (-h)^m / real(fact m)) =
     1.6                      (\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))")
     1.7 -apply (rule_tac [2] sumr_fun_eq)
     1.8 +apply (rule_tac [2] setsum_cong[OF refl])
     1.9  apply (auto simp add: divide_inverse power_mult_distrib [symmetric])
    1.10  done
    1.11  
    1.12 @@ -435,7 +435,7 @@
    1.13  apply (drule_tac x = x in spec, simp)
    1.14  apply (erule ssubst)
    1.15  apply (rule_tac x = t in exI, simp)
    1.16 -apply (rule sumr_fun_eq)
    1.17 +apply (rule setsum_cong[OF refl])
    1.18  apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
    1.19  done
    1.20  
    1.21 @@ -465,7 +465,7 @@
    1.22  apply (simp (no_asm) add: times_divide_eq)
    1.23  apply (erule ssubst)
    1.24  apply (rule_tac x = t in exI, simp)
    1.25 -apply (rule sumr_fun_eq)
    1.26 +apply (rule setsum_cong[OF refl])
    1.27  apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
    1.28  done
    1.29  
    1.30 @@ -483,7 +483,7 @@
    1.31  apply (simp (no_asm) add: times_divide_eq)
    1.32  apply (erule ssubst)
    1.33  apply (rule_tac x = t in exI, simp)
    1.34 -apply (rule sumr_fun_eq)
    1.35 +apply (rule setsum_cong[OF refl])
    1.36  apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
    1.37  done
    1.38  
    1.39 @@ -516,7 +516,7 @@
    1.40  apply (drule_tac x = x in spec, simp)
    1.41  apply (erule ssubst)
    1.42  apply (rule_tac x = t in exI, simp)
    1.43 -apply (rule sumr_fun_eq)
    1.44 +apply (rule setsum_cong[OF refl])
    1.45  apply (auto simp add: cos_zero_iff even_mult_two_ex)
    1.46  done
    1.47  
    1.48 @@ -535,7 +535,7 @@
    1.49  apply (simp (no_asm) add: times_divide_eq)
    1.50  apply (erule ssubst)
    1.51  apply (rule_tac x = t in exI, simp)
    1.52 -apply (rule sumr_fun_eq)
    1.53 +apply (rule setsum_cong[OF refl])
    1.54  apply (auto simp add: cos_zero_iff even_mult_two_ex)
    1.55  done
    1.56  
    1.57 @@ -554,7 +554,7 @@
    1.58  apply (simp (no_asm) add: times_divide_eq)
    1.59  apply (erule ssubst)
    1.60  apply (rule_tac x = t in exI, simp)
    1.61 -apply (rule sumr_fun_eq)
    1.62 +apply (rule setsum_cong[OF refl])
    1.63  apply (auto simp add: cos_zero_iff even_mult_two_ex)
    1.64  done
    1.65  
    1.66 @@ -585,10 +585,10 @@
    1.67      apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
    1.68      apply (erule ssubst)
    1.69      apply (rule sin_bound_lemma)
    1.70 -    apply (rule sumr_fun_eq, safe)
    1.71 -    apply (rule_tac f = "%u. u * (x^r)" in arg_cong)
    1.72 +    apply (rule setsum_cong[OF refl])
    1.73 +    apply (rule_tac f = "%u. u * (x^xa)" in arg_cong)
    1.74      apply (subst even_even_mod_4_iff)
    1.75 -    apply (cut_tac m=r in mod_exhaust_less_4, simp, safe)
    1.76 +    apply (cut_tac m=xa in mod_exhaust_less_4, simp, safe)
    1.77      apply (simp_all add:even_num_iff)
    1.78      apply (drule lemma_even_mod_4_div_2[simplified])
    1.79      apply(simp add: numeral_2_eq_2 divide_inverse)