Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/IOA/TLS.thy
changeset 80914 d97fdabd9e2b
parent 71989 bad75618fb82 
--- a/src/HOL/HOLCF/IOA/TLS.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -42,7 +42,7 @@
 definition ex2seq :: "('a, 's) execution \<Rightarrow> ('a option, 's) transition Seq"
   where "ex2seq ex = (ex2seqC \<cdot> (mkfin (snd ex))) (fst ex)"
 
-definition temp_sat :: "('a, 's) execution \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool"  (infixr "\<TTurnstile>" 22)
+definition temp_sat :: "('a, 's) execution \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool"  (infixr \<open>\<TTurnstile>\<close> 22)
   where "(ex \<TTurnstile> P) \<longleftrightarrow> ((ex2seq ex) \<Turnstile> P)"
 
 definition validTE :: "('a, 's) ioa_temp \<Rightarrow> bool"
isabelle