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/Comp.thy
changeset 80914 d97fdabd9e2b
parent 63146 f1ecba0272f9 
--- a/src/HOL/UNITY/Comp.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/Comp.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -25,10 +25,10 @@
 
 end
 
-definition component_of :: "'a program =>'a program=> bool" (infixl "component'_of" 50)
+definition component_of :: "'a program =>'a program=> bool" (infixl \<open>component'_of\<close> 50)
   where "F component_of H == \<exists>G. F ok G & F\<squnion>G = H"
 
-definition strict_component_of :: "'a program\<Rightarrow>'a program=> bool" (infixl "strict'_component'_of" 50)
+definition strict_component_of :: "'a program\<Rightarrow>'a program=> bool" (infixl \<open>strict'_component'_of\<close> 50)
   where "F strict_component_of H == F component_of H & F\<noteq>H"
 
 definition preserves :: "('a=>'b) => 'a program set"
isabelle