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/Detects.thy
changeset 80914 d97fdabd9e2b
parent 63146 f1ecba0272f9 
--- a/src/HOL/UNITY/Detects.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/Detects.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -9,10 +9,10 @@
 
 theory Detects imports FP SubstAx begin
 
-definition Detects :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
+definition Detects :: "['a set, 'a set] => 'a program set"  (infixl \<open>Detects\<close> 60)
   where "A Detects B = (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
 
-definition Equality :: "['a set, 'a set] => 'a set"  (infixl "<==>" 60)
+definition Equality :: "['a set, 'a set] => 'a set"  (infixl \<open><==>\<close> 60)
   where "A <==> B = (-A \<union> B) \<inter> (A \<union> -B)"
isabelle