4 Isabelle2008 is now available. |
4 Isabelle2008 is now available. |
5 |
5 |
6 This release consolidates Isabelle2007, see the NEWS file in the |
6 This release consolidates Isabelle2007, see the NEWS file in the |
7 distribution for more details. Some notable improvements are: |
7 distribution for more details. Some notable improvements are: |
8 |
8 |
9 * New version of HOL 'primrec' supporting type-inference and local |
9 * HOL: significant speedup of Metis prover; proper support for |
10 theory targets. |
10 multithreading. |
|
11 |
|
12 * HOL: new version of 'primrec' command supporting type-inference and |
|
13 local theory targets. |
|
14 |
|
15 * HOL: improved support for termination proofs of recursive function |
|
16 definitions. |
11 |
17 |
12 * New local theory targets for class instantiation and overloading. |
18 * New local theory targets for class instantiation and overloading. |
13 |
19 |
14 * Support for named dynamic lists of theorems. |
20 * Support for named dynamic lists of theorems. |
15 |
|
16 * Significant speedup of Metis prover, with proper support for |
|
17 multithreading. |
|
18 |
21 |
19 * Simple TTY interface with command-line editing. |
22 * Simple TTY interface with command-line editing. |
20 |
23 |
21 * Improved support for the Cygwin platform (Windows). |
24 * Improved support for the Cygwin platform (Windows). |
22 |
25 |
23 * Support for Poly/ML 5.2 with improved handling of multithreading and |
26 * Support for Poly/ML 5.2 with improved handling of multithreading and |
24 external processes. |
27 external processes. |
25 |
28 |
26 * Reorganized version of Isabelle/Isar Reference Manual. |
29 * Reorganized and updated version of Isabelle/Isar Reference Manual. |
27 |
30 |
28 |
31 |
29 You may get Isabelle2008 from the following mirror sites: |
32 You may get Isabelle2008 from the following mirror sites: |
30 |
33 |
31 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |
34 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |