2 To: isabelle-users@cl.cam.ac.uk |
2 To: isabelle-users@cl.cam.ac.uk |
3 |
3 |
4 Isabelle2015 is now available. |
4 Isabelle2015 is now available. |
5 |
5 |
6 This version improves upon Isabelle2014 in many ways, see the NEWS file in |
6 This version improves upon Isabelle2014 in many ways, see the NEWS file in |
7 the distribution for more details. Important points are: |
7 the distribution for more details. Some important points are as follows. |
8 |
8 |
9 * FIXME |
9 * Improved Isabelle/jEdit Prover IDE: folding / bracket matching for Isar, |
|
10 support for BibTeX files, improved graphview panel, improved scheduling for |
|
11 asynchronous print commands (e.g. Slegehammer provers). |
|
12 |
|
13 * Support for 'private' and 'qualified' name space modifiers. |
|
14 |
|
15 * Structural composition of proof methods (meth1; meth2) in Isar. |
|
16 |
|
17 * HOL: BNF datatypes and codatatypes are now standard. |
|
18 |
|
19 * HOL: numerous tool improvements: Nitpick, Sledgehammer, SMT, including a |
|
20 new free (!) version of Z3. |
|
21 |
|
22 * HOL: numerous library refinements and enhancements. |
|
23 |
|
24 * New proof method "rewrite" for single-step rewriting with subterm |
|
25 selection based on patterns. |
|
26 |
|
27 * Updated manuals: datatypes, implementation, isar-ref, jedit, sledgehammer, |
|
28 system. |
10 |
29 |
11 |
30 |
12 You may get Isabelle2015 from the following mirror sites: |
31 You may get Isabelle2015 from the following mirror sites: |
13 |
32 |
14 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
33 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |