# HG changeset patch
# User desharna
# Date 1671433656 -3600
# Node ID 806d0b3aebafaf605498f61a93113262fa1aa17e
# Parent  3eda063a20a4242fb7c535ebacef95b2f838eed5
strengthened and renamed asymp_less and asymp_greater

diff -r 3eda063a20a4 -r 806d0b3aebaf NEWS
--- a/NEWS	Mon Dec 19 08:01:31 2022 +0100
+++ b/NEWS	Mon Dec 19 08:07:36 2022 +0100
@@ -43,6 +43,8 @@
   - 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.asymp_greater[simp] ~> preorder.asymp_on_greater[simp]
+      preorder.asymp_less[simp] ~> preorder.asymp_on_less[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 3eda063a20a4 -r 806d0b3aebaf src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 08:01:31 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 08:07:36 2022 +0100
@@ -385,11 +385,11 @@
 lemma asymp_on_subset: "asymp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asymp_on B R"
   by (auto simp: asymp_on_def)
 
-lemma (in preorder) asymp_less[simp]: "asymp (<)"
-  by (auto intro: asympI dual_order.asym)
+lemma (in preorder) asymp_on_less[simp]: "asymp_on A (<)"
+  by (auto intro: dual_order.asym)
 
-lemma (in preorder) asymp_greater[simp]: "asymp (>)"
-  by (auto intro: asympI dual_order.asym)
+lemma (in preorder) asymp_on_greater[simp]: "asymp_on A (>)"
+  by (auto intro: dual_order.asym)
 
 
 subsubsection \<open>Symmetry\<close>
@@ -581,10 +581,10 @@
   by (rule antisym_if_asym[to_pred])
 
 lemma (in preorder) antisymp_less[simp]: "antisymp (<)"
-  by (rule antisymp_if_asymp[OF asymp_less])
+  by (rule antisymp_if_asymp[OF asymp_on_less])
 
 lemma (in preorder) antisymp_greater[simp]: "antisymp (>)"
-  by (rule antisymp_if_asymp[OF asymp_greater])
+  by (rule antisymp_if_asymp[OF asymp_on_greater])
 
 lemma (in order) antisymp_on_le[simp]: "antisymp_on A (\<le>)"
   by (simp add: antisymp_onI)