NEWS

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