proper path specifications;
authorwenzelm
Tue Jul 31 23:23:34 2007 +0200 (2007-07-31)
changeset 24107fecafd71e758
parent 24106 f2965bf954dc
child 24108 24e5587603b4
proper path specifications;
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/FOCUS/Fstreams.thy
src/HOLCF/FOCUS/Stream_adm.thy
     1.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Tue Jul 31 23:23:28 2007 +0200
     1.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Tue Jul 31 23:23:34 2007 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  header {* FOCUS flat streams *}
     1.5  
     1.6  theory Fstream
     1.7 -imports Stream
     1.8 +imports "../ex/Stream"
     1.9  begin
    1.10  
    1.11  defaultsort type
     2.1 --- a/src/HOLCF/FOCUS/Fstreams.thy	Tue Jul 31 23:23:28 2007 +0200
     2.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy	Tue Jul 31 23:23:34 2007 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  ###TODO: integrate this with Fstream.*
     2.5  *)
     2.6  
     2.7 -theory Fstreams imports Stream begin
     2.8 +theory Fstreams imports "../ex/Stream" begin
     2.9  
    2.10  defaultsort type
    2.11  
     3.1 --- a/src/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 31 23:23:28 2007 +0200
     3.2 +++ b/src/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 31 23:23:34 2007 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Admissibility for streams *}
     3.5  
     3.6  theory Stream_adm
     3.7 -imports Stream Continuity
     3.8 +imports "../ex/Stream" Continuity
     3.9  begin
    3.10  
    3.11  definition