NEWS

--- a/NEWS	Thu Jul 27 15:22:35 2017 +0100
+++ b/NEWS	Fri Jul 28 15:36:32 2017 +0100
@@ -197,6 +197,9 @@
 Knaster-Tarski fixed point theorem and Galois Connections.
 
 * SMT module:
+  - A new option, 'smt_nat_as_int', has been added to translate 'nat' to
+    'int' and benefit from the SMT solver's theory reasoning. It is disabled
+    by default.
   - The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed.
   - Several small issues have been rectified in the 'smt' command.