# HG changeset patch
# User wenzelm
# Date 1573079111 -3600
# Node ID 9314a4cc84eabc865bb1dc947a9215ab3763eb72
# Parent  98ac9a4323a2faa3944f71d7aaea73124fe9c3e9# Parent  510b89906d863719135220be3d918d20b013be3e
merged

diff -r 510b89906d86 -r 9314a4cc84ea src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Wed Nov 06 23:24:16 2019 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Wed Nov 06 23:25:11 2019 +0100
@@ -455,7 +455,7 @@
 lemma ev_at_shift: "ev_at (HLD X) i (stake (Suc i) \<omega> @- \<omega>' :: 's stream) \<longleftrightarrow> ev_at (HLD X) i \<omega>"
   by (induction i arbitrary: \<omega>) (auto simp: HLD_iff)
 
-lemma ev_iff_ev_at_unqiue: "ev P \<omega> \<longleftrightarrow> (\<exists>!n. ev_at P n \<omega>)"
+lemma ev_iff_ev_at_unique: "ev P \<omega> \<longleftrightarrow> (\<exists>!n. ev_at P n \<omega>)"
   by (auto intro: ev_at_unique simp: ev_iff_ev_at)
 
 lemma alw_HLD_iff_streams: "alw (HLD X) \<omega> \<longleftrightarrow> \<omega> \<in> streams X"