--- a/src/HOL/Series.thy Tue Mar 26 12:20:58 2013 +0100 +++ b/src/HOL/Series.thy Tue Mar 26 12:20:58 2013 +0100 @@ -10,7 +10,7 @@ header{*Finite Summation and Infinite Series*} theory Series -imports SEQ Deriv +imports Deriv begin definition