# HG changeset patch
# User blanchet
# Date 1416828913 -3600
# Node ID 32145985352a25ea5dcec6b8cf6a0d1b3f85ec50
# Parent  e50f1973cb0a4103bcae038726391ed1642b0504
updated NEWS

diff -r e50f1973cb0a -r 32145985352a NEWS
--- a/NEWS	Mon Nov 24 12:35:13 2014 +0100
+++ b/NEWS	Mon Nov 24 12:35:13 2014 +0100
@@ -141,10 +141,17 @@
 
 * Product over lists via constant "listprod".
 
+* Nitpick:
+  - Fixed soundness bug related to the strict and nonstrict subset
+    operations.
+
 * Sledgehammer:
   - Minimization is now always enabled by default.
     Removed subcommand:
       min
+  - The proof reconstruction, both one-liners and Isar, has been
+    dramatically improved.
+  - Improved support for CVC4 and veriT.
 
 * Old and new SMT modules:
   - The old 'smt' method has been renamed 'old_smt' and moved to