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