NEWS

--- a/NEWS	Thu Apr 20 10:45:52 2017 +0200
+++ b/NEWS	Thu Apr 20 16:21:28 2017 +0200
@@ -154,6 +154,8 @@
 * 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.
+
 * Session HOL-Analysis: more material involving arcs, paths, covering
 spaces, innessential maps, retracts. Major results include the Jordan
 Curve Theorem and the Great Picard Theorem.