--- 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]
--- 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"
--- 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)