src/HOL/Library/Preorder.thy
changeset 81142 6ad2c917dd2e
parent 80914 d97fdabd9e2b
--- a/src/HOL/Library/Preorder.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Preorder.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -14,7 +14,7 @@
 
 notation
   equiv (\<open>'(\<approx>')\<close>) and
-  equiv (\<open>(_/ \<approx> _)\<close>  [51, 51] 50)
+  equiv (\<open>(\<open>notation=\<open>infix \<approx>\<close>\<close>_/ \<approx> _)\<close>  [51, 51] 50)
 
 lemma equivD1: "x \<le> y" if "x \<approx> y"
   using that by (simp add: equiv_def)