src/HOL/Series.thy
changeset 29197 6d4cb27ed19c
parent 28952 15a4b2cf8c34
child 29803 c56a5571f60a
--- a/src/HOL/Series.thy	Mon Dec 29 13:23:53 2008 +0100
+++ b/src/HOL/Series.thy	Mon Dec 29 14:08:08 2008 +0100
@@ -10,7 +10,7 @@
 header{*Finite Summation and Infinite Series*}
 
 theory Series
-imports "~~/src/HOL/Hyperreal/SEQ"
+imports SEQ
 begin
 
 definition