# HG changeset patch
# User desharna
# Date 1741972298 -3600
# Node ID a317d9e27a038015284c111979afdde8fa628b78
# Parent  f7e08143eea2bee00b4b7e04ae23aed19819c38e
Strengthened and renamed lemmas antisymp_equality and transp_equality

diff -r f7e08143eea2 -r a317d9e27a03 NEWS
--- a/NEWS	Fri Mar 14 18:04:14 2025 +0100
+++ b/NEWS	Fri Mar 14 18:11:38 2025 +0100
@@ -22,6 +22,9 @@
     the formula "r \<subset> A \<times> A \<and> refl_on A r". INCOMPATIBILITY.
   - Strengthened lemmas. Minor INCOMPATIBILITY.
       refl_on_empty[simp]
+  - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
+      antisymp_equality[simp] ~> antisymp_on_equality[simp]
+      transp_equality[simp] ~> transp_on_equality[simp]
   - Added lemmas.
       reflp_on_refl_on_eq[pred_set_conv]
 
diff -r f7e08143eea2 -r a317d9e27a03 src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Fri Mar 14 18:04:14 2025 +0100
+++ b/src/HOL/Probability/SPMF.thy	Fri Mar 14 18:11:38 2025 +0100
@@ -1482,7 +1482,7 @@
 next
   fix x y z
   assume "?R x y" "?R y z"
-  with transp_ord_option[OF transp_equality] show "?R x z" by(rule transp_rel_pmf[THEN transpD])
+  with transp_ord_option[OF transp_on_equality] show "?R x z" by(rule transp_rel_pmf[THEN transpD])
 next
   fix x y
   assume "?R x y" "?R y x"
diff -r f7e08143eea2 -r a317d9e27a03 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Mar 14 18:04:14 2025 +0100
+++ b/src/HOL/Relation.thy	Fri Mar 14 18:11:38 2025 +0100
@@ -589,9 +589,8 @@
   "antisymp \<bottom>"
   by (fact antisym_empty [to_pred])
     
-lemma antisymp_equality [simp]:
-  "antisymp HOL.eq"
-  by (auto intro: antisympI)
+lemma antisymp_on_equality[simp]: "antisymp_on A (=)"
+  by (auto intro: antisymp_onI)
 
 lemma antisym_singleton [simp]:
   "antisym {x}"
@@ -715,8 +714,8 @@
 lemma transp_trans: "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   by (simp add: trans_def transp_def)
 
-lemma transp_equality [simp]: "transp (=)"
-  by (auto intro: transpI)
+lemma transp_on_equality[simp]: "transp_on A (=)"
+  by (auto intro: transp_onI)
 
 lemma trans_empty [simp]: "trans {}"
   by (blast intro: transI)