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