# HG changeset patch
# User desharna
# Date 1671103921 -3600
# Node ID e9f3f2b0c0a70f28ebfd80ff8d29d513c1d5418e
# Parent  8eb23d34323b9c38b7db5c360af83e04c21aa601
strengthened antisymp_le and antisymp_ge

diff -r 8eb23d34323b -r e9f3f2b0c0a7 NEWS
--- 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]
diff -r 8eb23d34323b -r e9f3f2b0c0a7 src/HOL/Relation.thy
--- 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>