1 |
1 |
2 Subject: Announcing Isabelle99-1 |
2 Subject: Announcing Isabelle99-2 |
3 To: isabelle-users@cl.cam.ac.uk |
3 To: isabelle-users@cl.cam.ac.uk |
4 |
4 |
5 Isabelle99-1 is now available. This release continues the line of |
5 Isabelle99-2 is now available. This release continues the line of |
6 Isabelle99, introducing numerous improvements, both internal and user |
6 Isabelle99, introducing various improvements in robustness and |
7 visible. |
7 usability. |
8 |
8 |
9 In particular, great care has been taken to improve robustness and |
9 The most prominent highlights of Isabelle99-2 are as follows. See the |
10 ease use and installation of the complete Isabelle working |
|
11 environment. This includes Proof General user interface support, WWW |
|
12 presentation of theories and the Isabelle document preparation system. |
|
13 |
|
14 The most prominent highlights of Isabelle99-1 are as follows. See the |
|
15 NEWS file distributed with Isabelle for more details. |
10 NEWS file distributed with Isabelle for more details. |
16 |
11 |
17 * Isabelle/Isar improvements (Markus Wenzel) |
12 * Poly/ML 4.0 used by default |
18 o Support of tactic-emulation scripts for easy porting of legacy ML |
13 More robust, less disk space required. |
19 scripts (see also the HOL/Lambda example). |
|
20 o Better support for scalable verification tasks (manage large |
|
21 contexts in induction, generalized existence reasoning etc.) |
|
22 o Hindley-Milner polymorphism for proof texts. |
|
23 o More robust document preparation, better LaTeX output due to |
|
24 fake math-mode. |
|
25 o Extended "Isabelle/Isar Reference Manual". |
|
26 |
14 |
27 * HOL/Algebra (Clemens Ballarin) |
15 * Pure/Simplifier (Stefan Berghofer) |
28 Rings and univariate polynomials. |
16 Proper implementation as a derived rule, outside the kernel! |
29 |
17 |
30 * HOL/BCV (Tobias Nipkow) |
18 * Isabelle/Isar (Markus Wenzel) |
31 Generic model of bytecode verification. |
19 Numerous usability improvements, e.g. support for initial |
|
20 schematic goals, failure prediction of subgoal statements, |
|
21 handling of non-atomic statements in induction. |
32 |
22 |
33 * HOL/IMPP (David von Oheimb) |
23 * Improved document preparation (Markus Wenzel) |
34 Extension of IMP with local variables and mutually recursive procedures. |
24 Near math-mode, sub/super scripts, more symbols etc. |
35 |
25 |
36 * HOL/Isar_examples (Markus Wenzel) |
26 * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson, |
37 More examples, including a formulation of Hoare Logic in Isabelle/Isar. |
27 Thomas M Rasmussen, Markus Wenzel) |
|
28 A collection of generic theories to be used together with main HOL. |
38 |
29 |
39 * HOL/Lambda (Stefan Berghofer and Tobias Nipkow) |
30 * HOL/Real and HOL/Hyperreal (Lawrence C Paulson and Jacques Fleuriot) |
40 More on termination of simply-typed lambda-terms (Isar script). |
31 General cleanup, more on nonstandard real analysis. |
41 |
32 |
42 * HOL/Lattice (Markus Wenzel) |
33 * HOL/Unix (Markus Wenzel) |
43 Lattices and orders in Isabelle/Isar. |
34 Some Aspects of Unix file-system security; demonstrates |
|
35 Isabelle/Isar in typical system modelling and verification tasks. |
44 |
36 |
45 * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and |
37 * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson) |
46 Cornelia Pusch) |
38 Extended version of the Isabelle/HOL tutorial. |
47 Formalization of a fragment of Java, together with a corresponding |
|
48 virtual machine and a specification of its bytecode verifier. |
|
49 |
39 |
50 * HOL/NumberTheory (Thomas Rasmussen) |
40 You may get Isabelle99-2 from any of the following mirror sites: |
51 Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, |
|
52 Fermat/Euler Theorem, Wilson's Theorem. |
|
53 |
|
54 * HOL/Prolog (David von Oheimb) |
|
55 A (bare-bones) implementation of Lambda-Prolog. |
|
56 |
|
57 * HOL/Real (Jacques Fleuriot) |
|
58 More on nonstandard real analysis. |
|
59 |
|
60 You may get Isabelle99-1 from any of the following mirror sites: |
|
61 |
41 |
62 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
42 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
63 Munich (Germany) http://isabelle.in.tum.de/dist/ |
43 Munich (Germany) http://isabelle.in.tum.de/dist/ |
64 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html |
44 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html |
65 Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html |
45 Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html |