src/HOL/Series.thy
changeset 51526 155263089e7b
parent 51477 2990382dc066
child 51528 66c3a7589de7
--- 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