updated for release;
authorwenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 620282ecee4679f99
parent 62027 b270f2b9bef8
child 62029 e18444532fce
updated for release;
ANNOUNCE
     1.1 --- a/ANNOUNCE	Fri Jan 01 16:39:10 2016 +0100
     1.2 +++ b/ANNOUNCE	Fri Jan 01 16:40:47 2016 +0100
     1.3 @@ -3,11 +3,28 @@
     1.4  
     1.5  Isabelle2016 is now available.
     1.6  
     1.7 -This version improves upon Isabelle2015 in numerous ways, see the NEWS
     1.8 -file in the distribution for further details. Some highlights are as
     1.9 -follows.
    1.10 +This version improves upon Isabelle2015 in many ways, see the NEWS file in the
    1.11 +distribution for further details. Some highlights are as follows:
    1.12 +
    1.13 +* Enhanced Isabelle/jEdit Prover IDE, with separate State versus Output panel
    1.14 +and more asynchronous task management within the prover/GUI.
    1.15 +
    1.16 +* Additional Isar language elements for structured statements and proofs.
    1.17 +
    1.18 +* Document language refinements, with Markdown-like text structure.
    1.19  
    1.20 -* FIXME
    1.21 +* More Isabelle symbols in theory and document sources.
    1.22 +
    1.23 +* Pure/HOL: uniform treatment of overloaded constant definitions versus type
    1.24 +definitions; upgrade of HOL typedef to definitional principle.
    1.25 +
    1.26 +* HOL tool enhancements: quickcheck, sledgehammer, nitpick, transfer.
    1.27 +
    1.28 +* Many HOL library improvements, including advanced topological concepts and
    1.29 +integration theory ported from HOL Light.
    1.30 +
    1.31 +* Upgrade to Poly/ML 5.6 with debugger IDE for Isabelle/ML and Standard ML,
    1.32 +per-thread profiling, native support for Windows (32bit and 64bit).
    1.33  
    1.34  
    1.35  You may get Isabelle2016 from the following mirror sites: