# HG changeset patch
# User blanchet
# Date 1497962489 -7200
# Node ID 1451a32479ba7c33b8c11b652ae906c8f6e32e55
# Parent  a1fb6beb27311fa6d906be2fe129100597514709
SMT news

diff -r a1fb6beb2731 -r 1451a32479ba NEWS
--- a/NEWS	Tue Jun 20 14:33:45 2017 +0200
+++ b/NEWS	Tue Jun 20 14:41:29 2017 +0200
@@ -162,7 +162,9 @@
 * Session HOL-Algebra extended by additional lattice theory: the
 Knaster-Tarski fixed point theorem and Galois Connections.
 
-* SMT module: The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed.
+* SMT module:
+  - The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed.
+  - Several small issues have been rectified in the 'smt' command.
 
 * Session HOL-Analysis: more material involving arcs, paths, covering
 spaces, innessential maps, retracts. Major results include the Jordan