src/HOL/Corec_Examples/Stream_Processor.thy
changeset 62726 5b2a7caa855b
parent 62698 9d706e37ddab
child 66453 cc19f7ca2ed6
equal deleted inserted replaced
62725:5ab1746186c7 62726:5b2a7caa855b
     5     Copyright   2014, 2016
     5     Copyright   2014, 2016
     6 
     6 
     7 Stream processors---a syntactic representation of continuous functions on streams.
     7 Stream processors---a syntactic representation of continuous functions on streams.
     8 *)
     8 *)
     9 
     9 
    10 section {* Stream Processors---A Syntactic Representation of Continuous Functions on Streams *}
    10 section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close>
    11 
    11 
    12 theory Stream_Processor
    12 theory Stream_Processor
    13 imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
    13 imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
    14 begin
    14 begin
    15 
    15