--- a/NEWS Thu Sep 07 23:13:15 2017 +0200
+++ b/NEWS Fri Sep 08 00:01:36 2017 +0200
@@ -134,6 +134,8 @@
*** HOL ***
+* The Nunchaku model finder is now part of "Main".
+
* 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
@@ -569,7 +571,7 @@
quantifier-free propositional logic with linear real arithmetic
including min/max/abs. See HOL/ex/Argo_Examples.thy for examples.
-* The new "nunchaku" program integrates the Nunchaku model finder. The
+* The new "nunchaku" command integrates the Nunchaku model finder. The
tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.
* Metis: The problem encoding has changed very slightly. This might