1 Subject: Announcing Isabelle2008 |
1 Subject: Announcing Isabelle2009 |
2 To: isabelle-users@cl.cam.ac.uk |
2 To: isabelle-users@cl.cam.ac.uk |
3 |
3 |
4 Isabelle2008 is now available. |
4 Isabelle2009 is now available. |
5 |
5 |
6 This release consolidates Isabelle2007, see the NEWS file in the |
6 This release significantly improves upon Isabelle2008, see the NEWS |
7 distribution for more details. Some notable improvements are: |
7 file in the distribution for more details. Some important changes |
|
8 are: |
8 |
9 |
9 * HOL: significant speedup of Metis prover; proper support for |
10 * Complete re-implementation of locales, with proper support for local |
10 multithreading. |
11 syntax, and more robust interpretation mechanism. |
11 |
12 |
12 * HOL: new version of 'primrec' command supporting type-inference and |
13 * New 'find_consts' and 'find_theorems' facilities, together with |
13 local theory targets. |
14 "auto solve" feature of toplevel goal statements. |
14 |
15 |
15 * HOL: improved support for termination proofs of recursive function |
16 * HOL: reorganization of main logic images. |
16 definitions. |
|
17 |
17 |
18 * New local theory targets for class instantiation and overloading. |
18 * HOL: improved implementation of Sledgehammer, based on generic ATP |
|
19 manager; support for remote ATPs. |
19 |
20 |
20 * Support for named dynamic lists of theorems. |
21 * HOL: numerous library improvements. |
21 |
22 |
22 * Simple TTY interface with command-line editing. |
23 * Updated and extended versions of main reference manuals. |
23 |
24 |
24 * Improved support for the Cygwin platform (Windows). |
25 * Simplified arrangement of Isabelle startup scripts and settings |
|
26 directory. |
25 |
27 |
26 * Support for Poly/ML 5.2 with improved handling of multithreading and |
28 * Simplified internal programming interfaces for all Isar language |
27 external processes. |
29 elements. |
28 |
30 |
29 * Reorganized and updated version of Isabelle/Isar Reference Manual. |
31 * General high-level support for concurrent ML programming. |
|
32 |
|
33 * Parallel proof checking within Isar theories. |
30 |
34 |
31 |
35 |
32 You may get Isabelle2008 from the following mirror sites: |
36 You may get Isabelle2009 from the following mirror sites: |
33 |
37 |
34 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
38 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
35 Munich (Germany) http://isabelle.in.tum.de/ |
39 Munich (Germany) http://isabelle.in.tum.de/ |
36 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ |
40 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ |