1 Subject: Announcing Isabelle2016 |
1 Subject: Announcing Isabelle2016 |
2 To: isabelle-users@cl.cam.ac.uk |
2 To: isabelle-users@cl.cam.ac.uk |
3 |
3 |
4 Isabelle2016 is now available. |
4 Isabelle2016 is now available. |
5 |
5 |
6 This version improves upon Isabelle2015 in numerous ways, see the NEWS |
6 This version improves upon Isabelle2015 in many ways, see the NEWS file in the |
7 file in the distribution for further details. Some highlights are as |
7 distribution for further details. Some highlights are as follows: |
8 follows. |
|
9 |
8 |
10 * FIXME |
9 * Enhanced Isabelle/jEdit Prover IDE, with separate State versus Output panel |
|
10 and more asynchronous task management within the prover/GUI. |
|
11 |
|
12 * Additional Isar language elements for structured statements and proofs. |
|
13 |
|
14 * Document language refinements, with Markdown-like text structure. |
|
15 |
|
16 * More Isabelle symbols in theory and document sources. |
|
17 |
|
18 * Pure/HOL: uniform treatment of overloaded constant definitions versus type |
|
19 definitions; upgrade of HOL typedef to definitional principle. |
|
20 |
|
21 * HOL tool enhancements: quickcheck, sledgehammer, nitpick, transfer. |
|
22 |
|
23 * Many HOL library improvements, including advanced topological concepts and |
|
24 integration theory ported from HOL Light. |
|
25 |
|
26 * Upgrade to Poly/ML 5.6 with debugger IDE for Isabelle/ML and Standard ML, |
|
27 per-thread profiling, native support for Windows (32bit and 64bit). |
11 |
28 |
12 |
29 |
13 You may get Isabelle2016 from the following mirror sites: |
30 You may get Isabelle2016 from the following mirror sites: |
14 |
31 |
15 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
32 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |