src/HOL/Library/Preorder.thy
changeset 80914 d97fdabd9e2b
parent 69821 8432b771f12e
child 81142 6ad2c917dd2e
--- a/src/HOL/Library/Preorder.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/Preorder.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -13,8 +13,8 @@
   where "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
 
 notation
-  equiv ("'(\<approx>')") and
-  equiv ("(_/ \<approx> _)"  [51, 51] 50)
+  equiv (\<open>'(\<approx>')\<close>) and
+  equiv (\<open>(_/ \<approx> _)\<close>  [51, 51] 50)
 
 lemma equivD1: "x \<le> y" if "x \<approx> y"
   using that by (simp add: equiv_def)