NEWS

--- a/NEWS	Mon Oct 24 21:14:38 2016 +0200
+++ b/NEWS	Mon Oct 24 22:42:07 2016 +0200
@@ -910,6 +910,9 @@
 * Renamed HOL/Quotient_Examples/FSet.thy to
 HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY.
 
+* The "nunchaku" program integrates the Nunchaku model finder. The tool
+is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.
+
 
 *** ML ***