NEWS
changeset 82282 919eb0e67930
parent 82280 7587b93032ba
child 82283 f7c5a010115a
--- a/NEWS	Sat Mar 15 19:40:10 2025 +0100
+++ b/NEWS	Sat Mar 15 20:17:03 2025 +0100
@@ -55,8 +55,8 @@
       quotient_disj_strong
 
 * Theory "HOL.Transfer":
-  - Moved right_unique from HOL.Transfer to HOL.Relation.
-    Minor INCOMPATIBILITY.
+  - Moved predicates left_unique and right_unique from HOL.Transfer to
+    HOL.Relation. Minor INCOMPATIBILITY.
   - Added lemmas.
       single_valuedp_eq_right_unique