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/SubstAx.thy
changeset 80914 d97fdabd9e2b
parent 67613 ce654b0e6d69 
--- a/src/HOL/UNITY/SubstAx.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -9,13 +9,13 @@
 
 theory SubstAx imports WFair Constrains begin
 
-definition Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) where
+definition Ensures :: "['a set, 'a set] => 'a program set" (infixl \<open>Ensures\<close> 60) where
     "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}"
 
-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
     "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
 
-notation LeadsTo  (infixl "\<longmapsto>w" 60)
+notation LeadsTo  (infixl \<open>\<longmapsto>w\<close> 60)
 
 
 text\<open>Resembles the previous definition of LeadsTo\<close>
isabelle