--- a/ANNOUNCE Tue Jul 01 14:05:05 2014 +0200
+++ b/ANNOUNCE Tue Jul 01 14:52:08 2014 +0200
@@ -1,27 +1,36 @@
-Subject: Announcing Isabelle2013-2
+Subject: Announcing Isabelle2014
To: isabelle-users@cl.cam.ac.uk
-Isabelle2013-2 is now available.
+Isabelle2014 is now available.
+
+This version significantly improves upon Isabelle2013-2, see the NEWS
+file in the distribution for more details. Some highlights are:
-This version supersedes Isabelle2013-1, which in turn consolidated
-Isabelle2013 and introduced numerous improvements. See the NEWS file
-in the distribution for more details. Some highlights are:
+* Improved Isabelle/jEdit Prover IDE: navigation, completion,
+ spell-checking, Query panel, Simplifier Trace panel.
-* Significantly improved Isabelle/jEdit Prover IDE.
+* Support for auxiliary files within the Prover IDE.
-* Consolidated multi-platform support: Linux, Windows, Mac OS X.
+* Support for official Standard ML within the Prover IDE,
+ independently of Isabelle theory and proof development.
-* Added and updated manuals: datatypes, implementation, isar-ref, jedit.
+* HOL: BNF datatypes and codatatypes within theory Main, with numerous
+ add-on tools.
-* New Spec_Check tool: Quickcheck for Isabelle/ML.
+* HOL tool enhancements: Nitpick, Sledgehammer.
+
+* HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis,
+ HOL-Probability.
-* HOL library enhancements: Complex_Main, HOL-Library,
- HOL-Multivariate_Analysis.
+* HOL: internal SAT solver "cdclite" with models and proof traces.
+
+* HOL: updated SMT module, with support for SMT-LIB 2 and recent
+ versions of Z3, as well as CVC3, CVC4.
-* HOL tool enhancements: Codegenerator, Function, Lifting, Transfer,
- Nitpick, Sledgehammer.
+* Updated and extended manuals: codegen, datatypes, implementation,
+ isar-ref, jedit, system.
-* HOL-BNF: significantly improved BNF-based (co)datatype package.
+* System integration: improved support of LateX on Windows platform.
You may get Isabelle2013-2 from the following mirror sites: