diff -r 3b10acac1d5e -r ecad2a53755a ANNOUNCE --- 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: