Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
corrected typo in lemma name
authortraytel
Wed, 06 Nov 2019 16:57:51 +0100
changeset 71064 c9c1a64eeb69
parent 71062 b3956a37c994
child 71065 98ac9a4323a2
corrected typo in lemma name
src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle