--- a/src/HOLCF/FOCUS/Fstream.thy Tue Jul 31 23:23:28 2007 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Tue Jul 31 23:23:34 2007 +0200
@@ -9,7 +9,7 @@
header {* FOCUS flat streams *}
theory Fstream
-imports Stream
+imports "../ex/Stream"
begin
defaultsort type
--- a/src/HOLCF/FOCUS/Fstreams.thy Tue Jul 31 23:23:28 2007 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy Tue Jul 31 23:23:34 2007 +0200
@@ -6,7 +6,7 @@
###TODO: integrate this with Fstream.*
*)
-theory Fstreams imports Stream begin
+theory Fstreams imports "../ex/Stream" begin
defaultsort type
--- a/src/HOLCF/FOCUS/Stream_adm.thy Tue Jul 31 23:23:28 2007 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Tue Jul 31 23:23:34 2007 +0200
@@ -6,7 +6,7 @@
header {* Admissibility for streams *}
theory Stream_adm
-imports Stream Continuity
+imports "../ex/Stream" Continuity
begin
definition