changeset 57452 ecad2a53755a
parent 54639 5adc68deb322
child 57504 5cf245c62c4c
--- 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
-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: