diff -r 9bbc085fce86 -r 3042416b2e65 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Dec 16 10:23:51 2022 +0100
+++ b/src/HOL/Relation.thy	Fri Dec 16 10:28:37 2022 +0100
@@ -408,15 +408,17 @@
   obtains "r a b"
   using assms by (rule symE [to_pred])
 
-lemma symD [dest?]:
-  assumes "sym r" and "(b, a) \<in> r"
-  shows "(a, b) \<in> r"
-  using assms by (rule symE)
+lemma sym_onD: "sym_on A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r"
+  by (simp add: sym_on_def)
+
+lemma symD [dest?]: "sym r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r"
+  by (simp add: sym_onD)
 
-lemma sympD [dest?]:
-  assumes "symp r" and "r b a"
-  shows "r a b"
-  using assms by (rule symD [to_pred])
+lemma symp_onD: "symp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y x"
+  by (rule sym_onD[to_pred])
+
+lemma sympD [dest?]: "symp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
+  by (rule symD[to_pred])
 
 lemma sym_Int: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)"
   by (fast intro: symI elim: symE)