1 |
1 |
2 Subject: Announcing Isabelle99-2 |
2 Subject: Announcing Isabelle2001 |
3 To: isabelle-users@cl.cam.ac.uk |
3 To: isabelle-users@cl.cam.ac.uk |
4 |
4 |
5 Isabelle99-2 is now available. This release continues the line of |
5 Isabelle2001 is now available. |
6 Isabelle99, introducing various improvements in robustness and |
|
7 usability. |
|
8 |
6 |
9 The most prominent highlights of Isabelle99-2 are as follows. See the |
7 The most prominent highlights of Isabelle2001 are as follows. See the |
10 NEWS file distributed with Isabelle for more details. |
8 NEWS file distributed with Isabelle for more details. |
11 |
9 |
12 * Poly/ML 4.0 used by default |
10 * Specific support for Poly/ML 4.1.1 |
13 More robust, less disk space required. |
11 Faster, manages large heaps. |
14 |
12 |
15 * Simplifier (Stefan Berghofer) |
13 * Meta-level proof terms (Stefan Berghofer) |
16 Proper implementation as a derived rule, outside the kernel! |
|
17 |
14 |
18 * Improved document preparation (Markus Wenzel) |
15 You may get Isabelle2001 from any of the following mirror sites: |
19 Near math-mode, sub/super scripts, more symbols etc. |
|
20 |
|
21 * Isabelle/Isar (Markus Wenzel) |
|
22 Numerous usability improvements, e.g. support for initial |
|
23 schematic goals, failure prediction of subgoal statements, |
|
24 handling of non-atomic statements in induction. |
|
25 |
|
26 * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson, |
|
27 Thomas M Rasmussen, Markus Wenzel) |
|
28 A collection of generic theories to be used together with main HOL. |
|
29 |
|
30 * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson) |
|
31 General cleanup, more on nonstandard real analysis. |
|
32 |
|
33 * HOL/Unix (Markus Wenzel) |
|
34 Some Aspects of Unix file-system security; demonstrates |
|
35 Isabelle/Isar in typical system modelling and verification tasks. |
|
36 |
|
37 * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson) |
|
38 Extended version of the Isabelle/HOL tutorial. |
|
39 |
|
40 You may get Isabelle99-2 from any of the following mirror sites: |
|
41 |
16 |
42 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
17 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
43 Munich (Germany) http://isabelle.in.tum.de/dist/ |
18 Munich (Germany) http://isabelle.in.tum.de/dist/ |
44 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html |
19 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html |
45 Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html |
20 Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html |