--- a/NEWS Fri Mar 14 18:11:38 2025 +0100
+++ b/NEWS Fri Mar 14 18:13:56 2025 +0100
@@ -27,6 +27,7 @@
transp_equality[simp] ~> transp_on_equality[simp]
- Added lemmas.
reflp_on_refl_on_eq[pred_set_conv]
+ symp_on_equality[simp]
* Theory "HOL.Wellfounded":
- Added lemmas.
--- a/src/HOL/Relation.thy Fri Mar 14 18:11:38 2025 +0100
+++ b/src/HOL/Relation.thy Fri Mar 14 18:13:56 2025 +0100
@@ -477,6 +477,9 @@
lemma sympD [dest?]: "symp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
by (rule symD[to_pred])
+lemma symp_on_equality[simp]: "symp_on A (=)"
+ by (simp add: symp_on_def)
+
lemma sym_Int: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)"
by (fast intro: symI elim: symE)