src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
changeset 64911 f0e07600de47
parent 64320 ba194424b895
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Tue Jan 17 11:26:21 2017 +0100
     1.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Tue Jan 17 13:59:10 2017 +0100
     1.3 @@ -773,8 +773,8 @@
     1.4    shows "\<exists>x\<in>s. alw (ev (HLD {x})) \<omega>"
     1.5  proof -
     1.6    have "\<forall>i\<in>UNIV. \<exists>x\<in>s. \<omega> !! i = x"
     1.7 -    using `alw (HLD s) \<omega>` by (simp add: alw_iff_sdrop HLD_iff)
     1.8 -  from pigeonhole_infinite_rel[OF infinite_UNIV_nat `finite s` this]
     1.9 +    using \<open>alw (HLD s) \<omega>\<close> by (simp add: alw_iff_sdrop HLD_iff)
    1.10 +  from pigeonhole_infinite_rel[OF infinite_UNIV_nat \<open>finite s\<close> this]
    1.11    show ?thesis
    1.12      by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
    1.13  qed