changeset 66453 | cc19f7ca2ed6 |
parent 62175 | 8ffc4d0e652d |
child 67613 | ce654b0e6d69 |
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy Fri Aug 18 20:47:47 2017 +0200 @@ -9,7 +9,7 @@ section \<open>FOCUS flat streams\<close> theory Fstream -imports "~~/src/HOL/HOLCF/Library/Stream" +imports "HOLCF-Library.Stream" begin default_sort type