# HG changeset patch
# User wenzelm
# Date 1336075649 -7200
# Node ID 2cc26ddd82983a57518484948e16c0d15f7a070e
# Parent  6ea205a4d7fd0627c434c3f92544570f46f9c61a
more NEWS;

diff -r 6ea205a4d7fd -r 2cc26ddd8298 NEWS
--- a/NEWS	Thu May 03 13:17:15 2012 +0200
+++ b/NEWS	Thu May 03 22:07:29 2012 +0200
@@ -754,6 +754,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