src/HOL/Lattice/Orders.thy

--- a/src/HOL/Lattice/Orders.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Lattice/Orders.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -17,7 +17,7 @@
 \<close>
 
 class leq =
-  fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sqsubseteq>" 50)
+  fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl \<open>\<sqsubseteq>\<close> 50)
 
 class quasi_order = leq +
   assumes leq_refl [intro?]: "x \<sqsubseteq> x"