# HG changeset patch
# User traytel
# Date 1573055871 -3600
# Node ID c9c1a64eeb6912591422beb9b9b679a85fafaefd
# Parent  b3956a37c99476571bfda9312da927dfdfdcb6b1
corrected typo in lemma name

diff -r b3956a37c994 -r c9c1a64eeb69 src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Wed Nov 06 16:38:58 2019 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Wed Nov 06 16:57:51 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"