# HG changeset patch
# User hoelzl
# Date 1364296859 -3600
# Node ID 66c3a7589de7019cf34ec59b5ff420010c31d15e
# Parent  bd62e7ff103bcf785af1342ede7621c1c6a2072c
Series.thy is based on Limits.thy and not Deriv.thy

diff -r bd62e7ff103b -r 66c3a7589de7 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Mar 26 12:20:59 2013 +0100
+++ b/src/HOL/Series.thy	Tue Mar 26 12:20:59 2013 +0100
@@ -10,7 +10,7 @@
 header{*Finite Summation and Infinite Series*}
 
 theory Series
-imports Deriv
+imports Limits
 begin
 
 definition