--- a/NEWS Sat Mar 15 14:10:23 2025 +0100
+++ b/NEWS Sat Mar 15 14:29:19 2025 +0100
@@ -16,7 +16,7 @@
monotone_on_inf_fun
monotone_on_sup_fun
-* Theory "HOL.Relations":
+* Theory "HOL.Relation":
- 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.
@@ -55,7 +55,7 @@
quotient_disj_strong
* Theory "HOL.Transfer":
- - Moved right_unique from HOL.Transfer to HOL.Relations.
+ - Moved right_unique from HOL.Transfer to HOL.Relation.
Minor INCOMPATIBILITY.
- Added lemmas.
single_valuedp_eq_right_unique