--- a/NEWS Thu Mar 13 16:00:48 2025 +0100
+++ b/NEWS Fri Mar 14 18:02:16 2025 +0100
@@ -20,6 +20,8 @@
- Changed definition of predicate refl_on to not constrain the domain
and range of the relation. To get the old semantics, explicitely use
the formula "r \<subset> A \<times> A \<and> refl_on A r". INCOMPATIBILITY.
+ - Added lemmas.
+ reflp_on_refl_on_eq[pred_set_conv]
* Theory "HOL.Wellfounded":
- Added lemmas.
--- a/src/HOL/Relation.thy Thu Mar 13 16:00:48 2025 +0100
+++ b/src/HOL/Relation.thy Fri Mar 14 18:02:16 2025 +0100
@@ -167,8 +167,10 @@
text \<open>@{thm [source] reflp_def} is for backward compatibility.\<close>
-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 reflp_on_refl_on_eq[pred_set_conv]: "reflp_on A (\<lambda>a b. (a, b) \<in> r) \<longleftrightarrow> refl_on A r"
+ by (simp add: refl_on_def reflp_on_def)
+
+lemmas reflp_refl_eq = reflp_on_refl_on_eq[of UNIV]
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)