ANNOUNCE
changeset 57452 ecad2a53755a
parent 54639 5adc68deb322
child 57504 5cf245c62c4c
     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 significantly improves upon Isabelle2013-2, see the NEWS
    1.12 +file in the distribution for more details.  Some highlights are:
    1.13  
    1.14 -This version supersedes Isabelle2013-1, which in turn consolidated
    1.15 -Isabelle2013 and introduced numerous improvements.  See the NEWS file
    1.16 -in the distribution for more details.  Some highlights are:
    1.17 +* Improved Isabelle/jEdit Prover IDE: navigation, completion,
    1.18 +  spell-checking, Query panel, Simplifier Trace panel.
    1.19  
    1.20 -* Significantly improved Isabelle/jEdit Prover IDE.
    1.21 +* Support for auxiliary files within the Prover IDE.
    1.22  
    1.23 -* Consolidated multi-platform support: Linux, Windows, Mac OS X.
    1.24 +* Support for official Standard ML within the Prover IDE,
    1.25 +  independently of Isabelle theory and proof development.
    1.26  
    1.27 -* Added and updated manuals: datatypes, implementation, isar-ref, jedit.
    1.28 +* HOL: BNF datatypes and codatatypes within theory Main, with numerous
    1.29 +  add-on tools.
    1.30  
    1.31 -* New Spec_Check tool: Quickcheck for Isabelle/ML.
    1.32 +* HOL tool enhancements: Nitpick, Sledgehammer.
    1.33 +
    1.34 +* HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis,
    1.35 +  HOL-Probability.
    1.36  
    1.37 -* HOL library enhancements: Complex_Main, HOL-Library,
    1.38 -  HOL-Multivariate_Analysis.
    1.39 +* HOL: internal SAT solver "cdclite" with models and proof traces.
    1.40 +
    1.41 +* HOL: updated SMT module, with support for SMT-LIB 2 and recent
    1.42 +  versions of Z3, as well as CVC3, CVC4.
    1.43  
    1.44 -* HOL tool enhancements: Codegenerator, Function, Lifting, Transfer,
    1.45 -  Nitpick, Sledgehammer.
    1.46 +* Updated and extended manuals: codegen, datatypes, implementation,
    1.47 +  isar-ref, jedit, system.
    1.48  
    1.49 -* HOL-BNF: significantly improved BNF-based (co)datatype package.
    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: