1.1 --- a/NEWS	Tue May 22 16:59:27 2012 +0200
     1.2 +++ b/NEWS	Wed May 23 12:02:27 2012 +0200
     1.3 @@ -758,6 +758,9 @@
     1.4  * New theory HOL/Library/DAList provides an abstract type for
     1.5  association lists with distinct keys.
     1.6  
     1.7 +* Session HOL/IMP: Added new theory of abstract interpretation of
     1.8 +annotated commands.
     1.9 +
    1.10  * Session HOL-Import: Re-implementation from scratch is faster,
    1.11  simpler, and more scalable.  Requires a proof bundle, which is
    1.12  available as an external component.  Discontinued old (and mostly