# HG changeset patch
# User desharna
# Date 1671182315 -3600
# Node ID d616622812b2054daa83a9b11d7c68949f08102b
# Parent  99d6e9217586d2351bf97aa82b83bb5f13fb60f2
added lemma symp_on_sym_on_eq[pred_set_conv]

diff -r 99d6e9217586 -r d616622812b2 NEWS
--- a/NEWS	Fri Dec 16 10:13:52 2022 +0100
+++ b/NEWS	Fri Dec 16 10:18:35 2022 +0100
@@ -79,6 +79,7 @@
       preorder.reflp_on_ge[simp]
       preorder.reflp_on_le[simp]
       reflp_on_conversp[simp]
+      symp_on_sym_on_eq[pred_set_conv]
       totalI
       totalp_on_converse[simp]
       totalp_on_singleton[simp]
diff -r 99d6e9217586 -r d616622812b2 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Dec 16 10:13:52 2022 +0100
+++ b/src/HOL/Relation.thy	Fri Dec 16 10:18:35 2022 +0100
@@ -381,8 +381,10 @@
 
 text \<open>@{thm [source] sym_def} and @{thm [source] symp_def} are for backward compatibility.\<close>
 
-lemma symp_sym_eq [pred_set_conv]: "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r"
-  by (simp add: sym_def symp_def)
+lemma symp_on_sym_on_eq[pred_set_conv]: "symp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym_on A r"
+  by (simp add: sym_on_def symp_on_def)
+
+lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
 lemma symI [intro?]: "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r"
   by (unfold sym_def) iprover