corrected typo in lemma name
authortraytel
Wed Nov 06 16:57:51 2019 +0100 (8 days ago ago)
changeset 71261c9c1a64eeb69
parent 71260 b3956a37c994
child 71263 98ac9a4323a2
corrected typo in lemma name
src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
     1.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Wed Nov 06 16:38:58 2019 +0100
     1.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Wed Nov 06 16:57:51 2019 +0100
     1.3 @@ -455,7 +455,7 @@
     1.4  lemma ev_at_shift: "ev_at (HLD X) i (stake (Suc i) \<omega> @- \<omega>' :: 's stream) \<longleftrightarrow> ev_at (HLD X) i \<omega>"
     1.5    by (induction i arbitrary: \<omega>) (auto simp: HLD_iff)
     1.6  
     1.7 -lemma ev_iff_ev_at_unqiue: "ev P \<omega> \<longleftrightarrow> (\<exists>!n. ev_at P n \<omega>)"
     1.8 +lemma ev_iff_ev_at_unique: "ev P \<omega> \<longleftrightarrow> (\<exists>!n. ev_at P n \<omega>)"
     1.9    by (auto intro: ev_at_unique simp: ev_iff_ev_at)
    1.10  
    1.11  lemma alw_HLD_iff_streams: "alw (HLD X) \<omega> \<longleftrightarrow> \<omega> \<in> streams X"