1 Subject: Announcing Isabelle2015 |
1 Subject: Announcing Isabelle2016 |
2 To: isabelle-users@cl.cam.ac.uk |
2 To: isabelle-users@cl.cam.ac.uk |
3 |
3 |
4 Isabelle2015 is now available. |
4 Isabelle2016 is now available. |
5 |
5 |
6 This version improves upon Isabelle2014 in many ways, see the NEWS file in |
6 This version improves upon Isabelle2015 in numerous ways, see the NEWS |
7 the distribution for more details. Some important points are as follows. |
7 file in the distribution for further details. Some highlights are as |
|
8 follows. |
8 |
9 |
9 * Improved Isabelle/jEdit Prover IDE: folding / bracket matching for Isar, |
10 * FIXME |
10 support for BibTeX files, improved graphview panel, improved scheduling for |
|
11 asynchronous print commands (e.g. Sledgehammer 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 * New Eisbach proof method language and "match" method. |
|
28 |
|
29 * Updated manuals: datatypes, implementation, isar-ref, jedit, sledgehammer, |
|
30 system. |
|
31 |
11 |
32 |
12 |
33 You may get Isabelle2015 from the following mirror sites: |
13 You may get Isabelle2016 from the following mirror sites: |
34 |
14 |
35 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
15 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
36 Munich (Germany) http://isabelle.in.tum.de/ |
16 Munich (Germany) http://isabelle.in.tum.de/ |
37 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ |
17 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ |