| changeset 61685 | 2b3772ecfdec |
| parent 61682 | f2c69a221055 |
| child 61694 | 6571c78c9667 |
--- a/NEWS Sun Nov 15 16:37:03 2015 +0100 +++ b/NEWS Mon Nov 16 12:37:46 2015 +0100 @@ -546,6 +546,8 @@ expose low-level facts of the internal construction only if the option "function_defs" is enabled. Rare INCOMPATIBILITY. +* Data_Structures: new and growing session of standard data structures. + * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. * Library/Omega_Words_Fun: Infinite words modeled as functions nat =>