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