1.1 --- a/ANNOUNCE	Thu Jan 18 15:17:59 2018 +0100
     1.2 +++ b/ANNOUNCE	Fri Jan 19 12:49:17 2018 +0100
     1.3 @@ -1,37 +1,34 @@
     1.4 -Subject: Announcing Isabelle2015
     1.5 +Subject: Announcing Isabelle2017
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2015 is now available.
     1.9 +Isabelle2017 is now available.
    1.10  
    1.11 -This version improves upon Isabelle2014 in many ways, see the NEWS file in
    1.12 -the distribution for more details. Some important points are as follows.
    1.13 +This version introduces many changes over Isabelle2016-1: see the NEWS
    1.14 +file for further details. Some notable points:
    1.15  
    1.16 -* Improved Isabelle/jEdit Prover IDE: folding / bracket matching for Isar,
    1.17 -support for BibTeX files, improved graphview panel, improved scheduling for
    1.18 -asynchronous print commands (e.g. Sledgehammer provers).
    1.19 +* Experimental support for Visual Studio Code as alternative PIDE front-end.
    1.20  
    1.21 -* Support for 'private' and 'qualified' name space modifiers.
    1.22 +* Improved Isabelle/jEdit Prover IDE: management of session sources
    1.23 +independently of editor buffers, removal of unused theories, explicit
    1.24 +indication of theory status, more careful auto-indentation.
    1.25  
    1.26 -* Structural composition of proof methods (meth1; meth2) in Isar.
    1.27 +* Session-qualified theory imports.
    1.28  
    1.29 -* HOL: BNF datatypes and codatatypes are now standard.
    1.30 +* Code generator improvements: support for statically embedded computations.
    1.31  
    1.32 -* HOL: numerous tool improvements: Nitpick, Sledgehammer, SMT, including a
    1.33 -new free (!) version of Z3.
    1.34 +* Numerous HOL library improvements.
    1.35  
    1.36 -* HOL: numerous library refinements and enhancements.
    1.37 +* More material in HOL-Algebra, HOL-Computational_Algebra and HOL-Analysis
    1.38 +(ported from HOL-Light).
    1.39  
    1.40 -* New proof method "rewrite" for single-step rewriting with subterm
    1.41 -selection based on patterns.
    1.42 +* Improved Nunchaku model finder, now in main HOL.
    1.43  
    1.44 -* New Eisbach proof method language and "match" method.
    1.45 +* SQL database support in Isabelle/Scala.
    1.46  
    1.47 -* Updated manuals: datatypes, implementation, isar-ref, jedit, sledgehammer,
    1.48 -system.
    1.49  
    1.50 +You may get Isabelle2017 from the following mirror sites:
    1.51  
    1.52 -You may get Isabelle2015 from the following mirror sites:
    1.53 -
    1.54 -  Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.55 -  Munich (Germany)     http://isabelle.in.tum.de/
    1.56 -  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/
    1.57 +  Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle
    1.58 +  Munich (Germany)     http://isabelle.in.tum.de
    1.59 +  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle
    1.60 +  Potsdam, NY (USA)    http://mirror.clarkson.edu/isabelle