NEWS
changeset 66614 1f1c5d85d232
parent 66599 34b20f7236ea
child 66641 ff2e0115fea4
     1.1 --- a/NEWS	Thu Sep 07 23:13:15 2017 +0200
     1.2 +++ b/NEWS	Fri Sep 08 00:01:36 2017 +0200
     1.3 @@ -134,6 +134,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* The Nunchaku model finder is now part of "Main".
     1.8 +
     1.9  * SMT module:
    1.10    - A new option, 'smt_nat_as_int', has been added to translate 'nat' to
    1.11      'int' and benefit from the SMT solver's theory reasoning. It is
    1.12 @@ -569,7 +571,7 @@
    1.13  quantifier-free propositional logic with linear real arithmetic
    1.14  including min/max/abs. See HOL/ex/Argo_Examples.thy for examples.
    1.15  
    1.16 -* The new "nunchaku" program integrates the Nunchaku model finder. The
    1.17 +* The new "nunchaku" command integrates the Nunchaku model finder. The
    1.18  tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details.
    1.19  
    1.20  * Metis: The problem encoding has changed very slightly. This might