changeset 66453 | cc19f7ca2ed6 |
parent 62726 | 5b2a7caa855b |
child 72170 | 7fa9605b226c |
--- a/src/HOL/Corec_Examples/Stream_Processor.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Corec_Examples/Stream_Processor.thy Fri Aug 18 20:47:47 2017 +0200 @@ -10,7 +10,7 @@ section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close> theory Stream_Processor -imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream" +imports "HOL-Library.BNF_Corec" "HOL-Library.Stream" begin datatype (discs_sels) ('a, 'b, 'c) sp\<^sub>\<mu> =