NEWS
changeset 66298 5ff9fe3fee66
parent 66278 978fb83b100c
child 66310 e8d2862ec203
     1.1 --- a/NEWS	Thu Jul 27 15:22:35 2017 +0100
     1.2 +++ b/NEWS	Fri Jul 28 15:36:32 2017 +0100
     1.3 @@ -197,6 +197,9 @@
     1.4  Knaster-Tarski fixed point theorem and Galois Connections.
     1.5  
     1.6  * SMT module:
     1.7 +  - A new option, 'smt_nat_as_int', has been added to translate 'nat' to
     1.8 +    'int' and benefit from the SMT solver's theory reasoning. It is disabled
     1.9 +    by default.
    1.10    - The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed.
    1.11    - Several small issues have been rectified in the 'smt' command.
    1.12