# HG changeset patch
# User berghofe
# Date 1120219617 -7200
# Node ID fce796ad9c2baf66ff5f6eed9f0ee7fa83895d67
# Parent  03bdf544a552710cf00460d9955dc3201889f9de
Simplified some proofs (thanks to strong_setsum_cong).

diff -r 03bdf544a552 -r fce796ad9c2b src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Fri Jul 01 14:05:41 2005 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Jul 01 14:06:57 2005 +0200
@@ -360,11 +360,8 @@
 lemma lemma_realpow_diff_sumr:
      "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =  
       y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
-apply (auto simp add: setsum_mult simp del: setsum_op_ivl_Suc)
-apply (rule setsum_cong[OF refl])
-apply (subst lemma_realpow_diff)
-apply (auto simp add: mult_ac)
-done
+by (auto simp add: setsum_mult lemma_realpow_diff mult_ac
+  simp del: setsum_op_ivl_Suc cong: strong_setsum_cong)
 
 lemma lemma_realpow_diff_sumr2:
      "x ^ (Suc n) - y ^ (Suc n) =  
@@ -468,9 +465,8 @@
 lemma lemma_termdiff1:
   "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
    (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)"
-apply (rule setsum_cong[OF refl])
-apply (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac)
-done
+by (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac
+  cong: strong_setsum_cong)
 
 lemma less_add_one: "m < n ==> (\<exists>d. n = m + d + Suc 0)"
 by (simp add: less_iff_Suc_add)