--- a/NEWS Sat Mar 15 09:17:46 2025 +0100
+++ b/NEWS Sat Mar 15 10:39:45 2025 +0100
@@ -53,6 +53,8 @@
quotient_disj_strong
* Theory "HOL.Transfer":
+ - Moved right_unique from HOL.Transfer to HOL.Relations.
+ Minor INCOMPATIBILITY.
- Added lemmas.
single_valuedp_eq_right_unique