NEWS

--- a/NEWS	Tue Mar 11 10:20:44 2025 +0100
+++ b/NEWS	Wed Mar 12 19:26:59 2025 +0100
@@ -14,6 +14,11 @@
       monotone_on_inf_fun
       monotone_on_sup_fun
 
+* Theory "HOL.Relations":
+  - 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 ⊂ A × A ∧ refl_on A r". INCOMPATIBILITY.
+
 * Theory "HOL.Wellfounded":
   - Added lemmas.
       bex_rtrancl_min_element_if_wf_on