src/HOL/Corec_Examples/Stream_Processor.thy
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> =