src/HOL/HOLCF/FOCUS/Fstreams.thy
changeset 41413 64cd30d6b0b8
parent 40774 0437dbc127b3
child 41431 138f414f14cb
equal deleted inserted replaced
41412:35f30e07fe0d 41413:64cd30d6b0b8
     5 
     5 
     6 TODO: integrate this with Fstream.
     6 TODO: integrate this with Fstream.
     7 *)
     7 *)
     8 
     8 
     9 theory Fstreams
     9 theory Fstreams
    10 imports Stream
    10 imports "~~/src/HOL/HOLCF/Library/Stream"
    11 begin
    11 begin
    12 
    12 
    13 default_sort type
    13 default_sort type
    14 
    14 
    15 types 'a fstream = "('a lift) stream"
    15 types 'a fstream = "('a lift) stream"