src/HOL/Probability/Stream_Space.thy
changeset 66453 cc19f7ca2ed6
parent 64320 ba194424b895
child 67399 eab6ce8368fa
--- a/src/HOL/Probability/Stream_Space.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Stream_Space.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,8 +4,8 @@
 theory Stream_Space
 imports
   Infinite_Product_Measure
-  "~~/src/HOL/Library/Stream"
-  "~~/src/HOL/Library/Linear_Temporal_Logic_on_Streams"
+  "HOL-Library.Stream"
+  "HOL-Library.Linear_Temporal_Logic_on_Streams"
 begin
 
 lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)"