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)"