--- 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