ANNOUNCE
changeset 64392 9456313b57ed
parent 64072 9f96e4da3064
child 64423 012b64bcd399
     1.1 --- a/ANNOUNCE	Tue Oct 25 12:14:17 2016 +0200
     1.2 +++ b/ANNOUNCE	Tue Oct 25 12:23:54 2016 +0200
     1.3 @@ -3,11 +3,27 @@
     1.4  
     1.5  Isabelle2016-1 is now available.
     1.6  
     1.7 -This version introduces significant changes over Isabelle2016, see the
     1.8 -NEWS file in the distribution for further details. Some highlights are
     1.9 -as follows:
    1.10 +This version introduces significant changes over Isabelle2016: see the NEWS
    1.11 +file for further details. Some notable points are as follows:
    1.12 +
    1.13 +* Improved Isabelle/jEdit Prover IDE: more support for formal text structure,
    1.14 +more visual feedback.
    1.15 +
    1.16 +* The Isabelle/ML IDE can load Isabelle/Pure into itself.
    1.17 +
    1.18 +* Improved Isar proof and specification elements.
    1.19  
    1.20 -* TBA
    1.21 +* HOL codatatype specifications: new commands for corecursive functions.
    1.22 +
    1.23 +* HOL tools: new Argo SMT solver, experimental Nunchaku model finder.
    1.24 +
    1.25 +* HOL library: improved HOL-Number_Theory and HOL-Library, especially theory
    1.26 +Multiset.
    1.27 +
    1.28 +* Reorganization of HOL-Probability versus and HOL-Analysis, with many new
    1.29 +theorems ported from HOL-Light.
    1.30 +
    1.31 +* Improved management of Poly/ML 5.6 processes and cumulative heap files.
    1.32  
    1.33  
    1.34  You may get Isabelle2016-1 from the following mirror sites: