diff -r fba16c509af0 -r e8c96013ea8a src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/Relation.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -151,7 +151,7 @@
 subsubsection \<open>Reflexivity\<close>
 
 definition refl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
-  where "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)"
+  where "refl_on A r \<longleftrightarrow> (\<forall>x\<in>A. (x, x) \<in> r)"
 
 abbreviation refl :: "'a rel \<Rightarrow> bool" \<comment> \<open>reflexivity over a type\<close>
   where "refl \<equiv> refl_on UNIV"
@@ -170,7 +170,7 @@
 lemma reflp_refl_eq [pred_set_conv]: "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r"
   by (simp add: refl_on_def reflp_def)
 
-lemma refl_onI [intro?]: "r \<subseteq> A \<times> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
+lemma refl_onI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
   unfolding refl_on_def by (iprover intro!: ballI)
 
 lemma reflI: "(\<And>x. (x, x) \<in> r) \<Longrightarrow> refl r"
@@ -186,12 +186,6 @@
 lemma refl_onD: "refl_on A r \<Longrightarrow> a \<in> A \<Longrightarrow> (a, a) \<in> r"
   unfolding refl_on_def by blast
 
-lemma refl_onD1: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<in> A"
-  unfolding refl_on_def by blast
-
-lemma refl_onD2: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A"
-  unfolding refl_on_def by blast
-
 lemma reflD: "refl r \<Longrightarrow> (a, a) \<in> r"
   unfolding refl_on_def by blast
 
@@ -252,10 +246,6 @@
 lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}"
 by (blast intro: refl_onI)
 
-lemma refl_on_def' [nitpick_unfold, code]:
-  "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
-  by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
-
 lemma reflp_on_equality [simp]: "reflp_on A (=)"
   by (simp add: reflp_on_def)
 
@@ -952,7 +942,7 @@
   by blast
 
 lemma refl_on_Id_on: "refl_on A (Id_on A)"
-  by (rule refl_onI [OF Id_on_subset_Times Id_onI])
+  by (rule refl_onI[OF Id_onI])
 
 lemma antisym_Id_on [simp]: "antisym (Id_on A)"
   unfolding antisym_def by blast