--- 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>)"