Series.thy is based on Limits.thy and not Deriv.thy
authorhoelzl
Tue Mar 26 12:20:59 2013 +0100 (2013-03-26)
changeset 5152866c3a7589de7
parent 51527 bd62e7ff103b
child 51529 2d2f59e6055a
Series.thy is based on Limits.thy and not Deriv.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Series.thy	Tue Mar 26 12:20:59 2013 +0100
     1.2 +++ b/src/HOL/Series.thy	Tue Mar 26 12:20:59 2013 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  header{*Finite Summation and Infinite Series*}
     1.5  
     1.6  theory Series
     1.7 -imports Deriv
     1.8 +imports Limits
     1.9  begin
    1.10  
    1.11  definition