--- a/src/HOL/Relation.thy Mon Nov 21 13:48:58 2022 +0100
+++ b/src/HOL/Relation.thy Mon Nov 21 13:53:04 2022 +0100
@@ -246,8 +246,8 @@
"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_equality [simp]: "reflp (=)"
- by (simp add: reflp_def)
+lemma reflp_on_equality [simp]: "reflp_on A (=)"
+ by (simp add: reflp_on_def)
lemma reflp_on_mono:
"reflp_on A R \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q"