NEWS
changeset 82284 a01ea04aa58f
parent 82283 f7c5a010115a
child 82285 d804c8e78ed3
--- a/NEWS	Sat Mar 15 20:27:25 2025 +0100
+++ b/NEWS	Sat Mar 15 20:33:19 2025 +0100
@@ -58,6 +58,9 @@
 * Theory "HOL.Transfer":
   - Moved predicates left_unique and right_unique from HOL.Transfer to
     HOL.Relation. Minor INCOMPATIBILITY.
+  - Removed lemmas. Minor INCOMPATIBILITY.
+      left_unique_iff (use left_unique_iff_Uniq instead)
+      right_unique_iff (use right_unique_iff_Uniq instead)
   - Added lemmas.
       single_valuedp_eq_right_unique