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)