1.1 --- a/ANNOUNCE	Wed Aug 22 12:47:53 2018 +0200
     1.2 +++ b/ANNOUNCE	Wed Aug 22 14:44:15 2018 +0200
     1.3 @@ -1,34 +1,37 @@
     1.4 -Subject: Announcing Isabelle2017
     1.5 +Subject: Announcing Isabelle2018
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2017 is now available.
     1.9 +Isabelle2018 is now available.
    1.10  
    1.11 -This version introduces many changes over Isabelle2016-1: see the NEWS
    1.12 -file for further details. Some notable points:
    1.13 +This version introduces many changes over Isabelle2017: see the NEWS
    1.14 +file for further details. Here are some notable points:
    1.15  
    1.16 -* Experimental support for Visual Studio Code as alternative PIDE front-end.
    1.17 +* Improved infix notation within terms.
    1.18  
    1.19 -* Improved Isabelle/jEdit Prover IDE: management of session sources
    1.20 -independently of editor buffers, removal of unused theories, explicit
    1.21 -indication of theory status, more careful auto-indentation.
    1.22 +* Improved syntax for formal comments, within terms and other languages.
    1.23  
    1.24 -* Session-qualified theory imports.
    1.25 +* Improved management of ROOT files and session-qualified theories.
    1.26  
    1.27 -* Code generator improvements: support for statically embedded computations.
    1.28 +* Various improvements of document preparation.
    1.29  
    1.30 -* Numerous HOL library improvements.
    1.31 +* Many Isabelle/jEdit improvements, including semantic IDE for BibTeX.
    1.32  
    1.33 -* More material in HOL-Algebra, HOL-Computational_Algebra and HOL-Analysis
    1.34 -(ported from HOL-Light).
    1.35 +* Numerous HOL library improvements, including HOL-Algebra.
    1.36  
    1.37 -* Improved Nunchaku model finder, now in main HOL.
    1.38 +* Substantial additions to HOL-Analysis.
    1.39  
    1.40 -* SQL database support in Isabelle/Scala.
    1.41 +* HOL-Library.Code_Lazy: code generation for lazy evaluation.
    1.42  
    1.43 +* HOL-Real_Asymp: tools for semi-automatic real asymptotics.
    1.44  
    1.45 -You may get Isabelle2017 from the following mirror sites:
    1.46 +* Isabelle server for reactive communication with other programs.
    1.47  
    1.48 -  Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle
    1.49 -  Munich (Germany)     http://isabelle.in.tum.de
    1.50 +* More uniform 64-bit platform support: smaller Isabelle application.
    1.51 +
    1.52 +
    1.53 +You may get Isabelle2018 from the following mirror sites:
    1.54 +
    1.55 +  Cambridge (UK)       https://www.cl.cam.ac.uk/research/hvg/Isabelle
    1.56 +  Munich (Germany)     https://isabelle.in.tum.de
    1.57    Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle
    1.58 -  Potsdam, NY (USA)    http://mirror.clarkson.edu/isabelle
    1.59 +  Potsdam, NY (USA)    https://mirror.clarkson.edu/isabelle