diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Lattice/Lattice.thy
--- 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>