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)