# HG changeset patch
# User nipkow
# Date 1220289424 -7200
# Node ID ba4de3022862dd19d82c92ac99efea963899b70f
# Parent  f6b2d19951710840d2fc8747c4550b5b5dd78e7b
moved lemma into SetInterval where it belongs

diff -r f6b2d1995171 -r ba4de3022862 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Mon Sep 01 19:16:40 2008 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Mon Sep 01 19:17:04 2008 +0200
@@ -669,13 +669,9 @@
 lemma exp_zero [simp]: "exp 0 = 1"
 unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
 
-lemma setsum_head2:
-  "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}"
-by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)
-
 lemma setsum_cl_ivl_Suc2:
   "(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))"
-by (simp add: setsum_head2 setsum_shift_bounds_cl_Suc_ivl
+by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl
          del: setsum_cl_ivl_Suc)
 
 lemma exp_series_add: