# HG changeset patch
# User desharna
# Date 1671434287 -3600
# Node ID ca258cf6c9779c4e3f126efd7769ac93000cd5f7
# Parent  87e7ab6aa40b09b561eb72ca52adaec940fa2ef1
strengthened and renamed lemmas antisymp_less and antisymp_greater

diff -r 87e7ab6aa40b -r ca258cf6c977 NEWS
--- 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]
diff -r 87e7ab6aa40b -r ca258cf6c977 src/HOL/Relation.thy
--- 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>)"