1 Subject: Announcing Isabelle2013-2 |
1 Subject: Announcing Isabelle2014 |
2 To: isabelle-users@cl.cam.ac.uk |
2 To: isabelle-users@cl.cam.ac.uk |
3 |
3 |
4 Isabelle2013-2 is now available. |
4 Isabelle2014 is now available. |
5 |
5 |
6 This version supersedes Isabelle2013-1, which in turn consolidated |
6 This version significantly improves upon Isabelle2013-2, see the NEWS |
7 Isabelle2013 and introduced numerous improvements. See the NEWS file |
7 file in the distribution for more details. Some highlights are: |
8 in the distribution for more details. Some highlights are: |
|
9 |
8 |
10 * Significantly improved Isabelle/jEdit Prover IDE. |
9 * Improved Isabelle/jEdit Prover IDE: navigation, completion, |
|
10 spell-checking, Query panel, Simplifier Trace panel. |
11 |
11 |
12 * Consolidated multi-platform support: Linux, Windows, Mac OS X. |
12 * Support for auxiliary files within the Prover IDE. |
13 |
13 |
14 * Added and updated manuals: datatypes, implementation, isar-ref, jedit. |
14 * Support for official Standard ML within the Prover IDE, |
|
15 independently of Isabelle theory and proof development. |
15 |
16 |
16 * New Spec_Check tool: Quickcheck for Isabelle/ML. |
17 * HOL: BNF datatypes and codatatypes within theory Main, with numerous |
|
18 add-on tools. |
17 |
19 |
18 * HOL library enhancements: Complex_Main, HOL-Library, |
20 * HOL tool enhancements: Nitpick, Sledgehammer. |
19 HOL-Multivariate_Analysis. |
|
20 |
21 |
21 * HOL tool enhancements: Codegenerator, Function, Lifting, Transfer, |
22 * HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis, |
22 Nitpick, Sledgehammer. |
23 HOL-Probability. |
23 |
24 |
24 * HOL-BNF: significantly improved BNF-based (co)datatype package. |
25 * HOL: internal SAT solver "cdclite" with models and proof traces. |
|
26 |
|
27 * HOL: updated SMT module, with support for SMT-LIB 2 and recent |
|
28 versions of Z3, as well as CVC3, CVC4. |
|
29 |
|
30 * Updated and extended manuals: codegen, datatypes, implementation, |
|
31 isar-ref, jedit, system. |
|
32 |
|
33 * System integration: improved support of LateX on Windows platform. |
25 |
34 |
26 |
35 |
27 You may get Isabelle2013-2 from the following mirror sites: |
36 You may get Isabelle2013-2 from the following mirror sites: |
28 |
37 |
29 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
38 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |