--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Tue Jan 17 13:59:10 2017 +0100
@@ -773,8 +773,8 @@
shows "\<exists>x\<in>s. alw (ev (HLD {x})) \<omega>"
proof -
have "\<forall>i\<in>UNIV. \<exists>x\<in>s. \<omega> !! i = x"
- using `alw (HLD s) \<omega>` by (simp add: alw_iff_sdrop HLD_iff)
- from pigeonhole_infinite_rel[OF infinite_UNIV_nat `finite s` this]
+ using \<open>alw (HLD s) \<omega>\<close> by (simp add: alw_iff_sdrop HLD_iff)
+ from pigeonhole_infinite_rel[OF infinite_UNIV_nat \<open>finite s\<close> this]
show ?thesis
by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
qed