# HG changeset patch
# User desharna
# Date 1741972436 -3600
# Node ID 365917fc6e313a31d13c234580b78947d5f2eb4c
# Parent  a317d9e27a038015284c111979afdde8fa628b78
added lemma symp_on_equality[simp]

diff -r a317d9e27a03 -r 365917fc6e31 NEWS
--- 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.
diff -r a317d9e27a03 -r 365917fc6e31 src/HOL/Relation.thy
--- 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)