changeset 46239 | fcfb4aa8e6e6 |
parent 46236 | ae79f2978a67 |
child 46301 | e2e52c7d25c9 |
--- a/NEWS Tue Jan 17 10:45:42 2012 +0100 +++ b/NEWS Tue Jan 17 11:15:36 2012 +0100 @@ -130,8 +130,8 @@ INCOMPATIBILITY. -* Theory HOL/Library/AList has been renamed to - AList_Impl. INCOMPATIBILITY. +* New theory HOL/Library/DAList provides an abstract type for association + lists with distinct keys. * 'datatype' specifications allow explicit sort constraints.