diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Preorder.thy --- 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 (\'(\')\) and - equiv (\(_/ \ _)\ [51, 51] 50) + equiv (\(\notation=\infix \\\_/ \ _)\ [51, 51] 50) lemma equivD1: "x \ y" if "x \ y" using that by (simp add: equiv_def)