1.1 --- a/ANNOUNCE	Tue Jul 01 14:05:05 2014 +0200
     1.2 +++ b/ANNOUNCE	Tue Jul 01 14:52:08 2014 +0200
     1.3 @@ -1,27 +1,36 @@
     1.4 -Subject: Announcing Isabelle2013-2
     1.5 +Subject: Announcing Isabelle2014
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2013-2 is now available.
     1.9 +Isabelle2014 is now available.
    1.10  
    1.11 -This version supersedes Isabelle2013-1, which in turn consolidated
    1.12 -Isabelle2013 and introduced numerous improvements.  See the NEWS file
    1.13 -in the distribution for more details.  Some highlights are:
    1.14 +This version significantly improves upon Isabelle2013-2, see the NEWS
    1.15 +file in the distribution for more details.  Some highlights are:
    1.16  
    1.17 -* Significantly improved Isabelle/jEdit Prover IDE.
    1.18 +* Improved Isabelle/jEdit Prover IDE: navigation, completion,
    1.19 +  spell-checking, Query panel, Simplifier Trace panel.
    1.20  
    1.21 -* Consolidated multi-platform support: Linux, Windows, Mac OS X.
    1.22 +* Support for auxiliary files within the Prover IDE.
    1.23  
    1.24 -* Added and updated manuals: datatypes, implementation, isar-ref, jedit.
    1.25 +* Support for official Standard ML within the Prover IDE,
    1.26 +  independently of Isabelle theory and proof development.
    1.27  
    1.28 -* New Spec_Check tool: Quickcheck for Isabelle/ML.
    1.29 +* HOL: BNF datatypes and codatatypes within theory Main, with numerous
    1.30 +  add-on tools.
    1.31  
    1.32 -* HOL library enhancements: Complex_Main, HOL-Library,
    1.33 -  HOL-Multivariate_Analysis.
    1.34 +* HOL tool enhancements: Nitpick, Sledgehammer.
    1.35  
    1.36 -* HOL tool enhancements: Codegenerator, Function, Lifting, Transfer,
    1.37 -  Nitpick, Sledgehammer.
    1.38 +* HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis,
    1.39 +  HOL-Probability.
    1.40  
    1.41 -* HOL-BNF: significantly improved BNF-based (co)datatype package.
    1.42 +* HOL: internal SAT solver "cdclite" with models and proof traces.
    1.43 +
    1.44 +* HOL: updated SMT module, with support for SMT-LIB 2 and recent
    1.45 +  versions of Z3, as well as CVC3, CVC4.
    1.46 +
    1.47 +* Updated and extended manuals: codegen, datatypes, implementation,
    1.48 +  isar-ref, jedit, system.
    1.49 +
    1.50 +* System integration: improved support of LateX on Windows platform.
    1.51  
    1.52  
    1.53  You may get Isabelle2013-2 from the following mirror sites: