# HG changeset patch
# User wenzelm
# Date 1185917014 -7200
# Node ID fecafd71e7581733d87452ce6065e912f9654c1a
# Parent  f2965bf954dcefed4a7f8713fe3135df2c62a7d0
proper path specifications;

diff -r f2965bf954dc -r fecafd71e758 src/HOLCF/FOCUS/Fstream.thy
--- 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
diff -r f2965bf954dc -r fecafd71e758 src/HOLCF/FOCUS/Fstreams.thy
--- 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
 
diff -r f2965bf954dc -r fecafd71e758 src/HOLCF/FOCUS/Stream_adm.thy
--- 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