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/Constrains.thy
changeset 80914 d97fdabd9e2b
parent 69313 b021008c5397 
--- a/src/HOL/UNITY/Constrains.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -32,10 +32,10 @@
   | Acts:  "[| act \<in> Acts F;  s \<in> reachable F;  (s,s') \<in> act |]
             ==> s' \<in> reachable F"
 
-definition Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) where
+definition Constrains :: "['a set, 'a set] => 'a program set" (infixl \<open>Co\<close> 60) where
     "A Co B == {F. F \<in> (reachable F \<inter> A)  co  B}"
 
-definition Unless  :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) where
+definition Unless  :: "['a set, 'a set] => 'a program set" (infixl \<open>Unless\<close> 60) where
     "A Unless B == (A-B) Co (A \<union> B)"
 
 definition Stable     :: "'a set => 'a program set" where
isabelle