--- a/NEWS Mon Dec 19 08:16:50 2022 +0100
+++ b/NEWS Mon Dec 19 08:18:07 2022 +0100
@@ -83,8 +83,8 @@
linorder.totalp_on_less[simp]
order.antisymp_ge[simp]
order.antisymp_le[simp]
- preorder.antisymp_greater[simp]
- preorder.antisymp_less[simp]
+ preorder.antisymp_on_greater[simp]
+ preorder.antisymp_on_less[simp]
preorder.reflp_on_ge[simp]
preorder.reflp_on_le[simp]
reflp_on_conversp[simp]
--- a/src/HOL/Relation.thy Mon Dec 19 08:16:50 2022 +0100
+++ b/src/HOL/Relation.thy Mon Dec 19 08:18:07 2022 +0100
@@ -582,10 +582,10 @@
lemma antisymp_on_if_asymp_on: "asymp_on A R \<Longrightarrow> antisymp_on A R"
by (rule antisym_on_if_asym_on[to_pred])
-lemma (in preorder) antisymp_less[simp]: "antisymp (<)"
+lemma (in preorder) antisymp_on_less[simp]: "antisymp_on A (<)"
by (rule antisymp_on_if_asymp_on[OF asymp_on_less])
-lemma (in preorder) antisymp_greater[simp]: "antisymp (>)"
+lemma (in preorder) antisymp_on_greater[simp]: "antisymp_on A (>)"
by (rule antisymp_on_if_asymp_on[OF asymp_on_greater])
lemma (in order) antisymp_on_le[simp]: "antisymp_on A (\<le>)"