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/UNITY/WFair.thy
changeset 80914 d97fdabd9e2b
parent 69597 ff784d5a5bfb 
--- a/src/HOL/UNITY/WFair.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/WFair.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -42,7 +42,7 @@
     "transient A == {F. \<exists>act\<in>Acts F. act``A \<subseteq> -A}"
 
 definition
-  ensures :: "['a set, 'a set] => 'a program set"       (infixl "ensures" 60) where
+  ensures :: "['a set, 'a set] => 'a program set"       (infixl \<open>ensures\<close> 60) where
     "A ensures B == (A-B co A \<union> B) \<inter> transient (A-B)"
 
 
@@ -59,7 +59,7 @@
   | Union:  "\<forall>A \<in> S. (A,B) \<in> leads F ==> (Union S, B) \<in> leads F"
 
 
-definition leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60) where
+definition leadsTo :: "['a set, 'a set] => 'a program set" (infixl \<open>leadsTo\<close> 60) where
      \<comment> \<open>visible version of the LEADS-TO relation\<close>
     "A leadsTo B == {F. (A,B) \<in> leads F}"
   
@@ -67,7 +67,7 @@
      \<comment> \<open>predicate transformer: the largest set that leads to \<^term>\<open>B\<close>\<close>
     "wlt F B == \<Union>{A. F \<in> A leadsTo B}"
 
-notation leadsTo  (infixl "\<longmapsto>" 60)
+notation leadsTo  (infixl \<open>\<longmapsto>\<close> 60)
 
 
 subsection\<open>transient\<close>
isabelle