--- a/NEWS Thu Dec 15 10:55:01 2022 +0100
+++ b/NEWS Thu Dec 15 12:32:01 2022 +0100
@@ -35,6 +35,8 @@
explicitly provided for backward compatibility but their usage is
discouraged. Minor INCOMPATIBILITY.
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
+ order.antisymp_ge[simp] ~> order.antisymp_on_ge[simp]
+ order.antisymp_le[simp] ~> order.antisymp_on_le[simp]
preorder.irreflp_greater[simp] ~> preorder.irreflp_on_greater[simp]
preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp]
reflp_equality[simp] ~> reflp_on_equality[simp]
--- a/src/HOL/Relation.thy Thu Dec 15 10:55:01 2022 +0100
+++ b/src/HOL/Relation.thy Thu Dec 15 12:32:01 2022 +0100
@@ -517,11 +517,11 @@
lemma (in preorder) antisymp_greater[simp]: "antisymp (>)"
by (rule antisymp_if_asymp[OF asymp_greater])
-lemma (in order) antisymp_le[simp]: "antisymp (\<le>)"
- by (simp add: antisympI)
+lemma (in order) antisymp_on_le[simp]: "antisymp_on A (\<le>)"
+ by (simp add: antisymp_onI)
-lemma (in order) antisymp_ge[simp]: "antisymp (\<ge>)"
- by (simp add: antisympI)
+lemma (in order) antisymp_on_ge[simp]: "antisymp_on A (\<ge>)"
+ by (simp add: antisymp_onI)
subsubsection \<open>Transitivity\<close>