# HG changeset patch
# User huffman
# Date 1162400222 -3600
# Node ID f0b5e6254a1f88276dfce64b139dac379d147635
# Parent  1c0805003c4fe6f749478640fa0996f27fca9d07
move DERIV_sumr from Series.thy to Lim.thy

diff -r 1c0805003c4f -r f0b5e6254a1f src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Wed Nov 01 17:14:16 2006 +0100
+++ b/src/HOL/Hyperreal/Lim.thy	Wed Nov 01 17:57:02 2006 +0100
@@ -766,6 +766,15 @@
 apply (blast intro: LIM_unique)
 done
 
+text{*Differentiation of finite sum*}
+
+lemma DERIV_sumr [rule_format (no_asm)]:
+     "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
+      --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
+apply (induct "n")
+apply (auto intro: DERIV_add)
+done
+
 text{*Alternative definition for differentiability*}
 
 lemma DERIV_LIM_iff:
diff -r 1c0805003c4f -r f0b5e6254a1f src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Wed Nov 01 17:14:16 2006 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Wed Nov 01 17:57:02 2006 +0100
@@ -10,7 +10,7 @@
 header{*Finite Summation and Infinite Series*}
 
 theory Series
-imports SEQ Lim
+imports SEQ
 begin
 
 definition
@@ -560,14 +560,4 @@
 apply (auto intro!: geometric_sums)
 done
 
-
-text{*Differentiation of finite sum*}
-
-lemma DERIV_sumr [rule_format (no_asm)]:
-     "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
-      --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
-apply (induct "n")
-apply (auto intro: DERIV_add)
-done
-
 end