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/Lattice/Lattice.thy
changeset 80914 d97fdabd9e2b
parent 69597 ff784d5a5bfb 
--- a/src/HOL/Lattice/Lattice.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Lattice/Lattice.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -24,10 +24,10 @@
 \<close>
 
 definition
-  meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<sqinter>" 70) where
+  meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl \<open>\<sqinter>\<close> 70) where
   "x \<sqinter> y = (THE inf. is_inf x y inf)"
 definition
-  join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<squnion>" 65) where
+  join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl \<open>\<squnion>\<close> 65) where
   "x \<squnion> y = (THE sup. is_sup x y sup)"
 
 text \<open>
isabelle