1 |
1 |
2 Subject: Announcing Isabelle99-1 |
2 Subject: Announcing Isabelle99-1 |
3 To: isabelle-users@cl.cam.ac.uk |
3 To: isabelle-users@cl.cam.ac.uk |
4 |
4 |
5 Isabelle99-1 is now available. |
5 Isabelle99-1 is now available. This release continues the line of |
|
6 Isabelle99, introducing numerous improvements, both internal and user |
|
7 visible. |
6 |
8 |
|
9 In particular, great care has been taken to improve robustness and |
|
10 ease use and installation of the complete Isabelle working |
|
11 environment, including the Proof General user interface support, WWW |
|
12 presentation of theories and the Isabelle document preparation system. |
7 |
13 |
8 The most prominent highlights are: |
14 The most prominent highlights of Isabelle99-1 are as follows. |
9 |
15 |
10 * |
16 * Isabelle/Isar improvements (Markus Wenzel) |
|
17 o Support of tactic-emulation scripts for easy porting of legacy ML |
|
18 scripts (see also the HOL/Lambda example). |
|
19 o Better support for scalable verification tasks (manage large |
|
20 contexts in induction, generalized existence reasoning etc.) |
|
21 o Hindley-Milner polymorphism for proof texts. |
|
22 o More robust document preparation, better LaTeX output due to |
|
23 fake math-mode. |
|
24 o Extended "Isabelle/Isar Reference Manual" |
|
25 http://isabelle.in.tum.de/doc/isar-ref.pdf |
|
26 |
|
27 * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and |
|
28 Cornelia Pusch) |
|
29 Formalization of a fragment of Java, together with a corresponding |
|
30 virtual machine and a specification of its bytecode verifier and a |
|
31 lightweight bytecode verifier, including proofs of type-safety. |
|
32 |
|
33 * HOL/Real (Jacques Fleuriot) |
|
34 More on nonstandard real analysis. |
|
35 |
|
36 * HOL/Algebra (Clemens Ballarin) |
|
37 Rings and univariate polynomials. |
|
38 |
|
39 * HOL/NumberTheory (Thomas Rasmussen) |
|
40 Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, |
|
41 Fermat/Euler Theorem, Wilson's Theorem. |
|
42 |
|
43 * HOL/Lambda (Stefan Berghofer and Tobias Nipkow) |
|
44 More on termination of simply-typed lambda-terms; converted into |
|
45 an Isabelle/Isar tactic emulation script. |
|
46 |
|
47 * HOL/Lattice (Markus Wenzel) |
|
48 Lattices and orders in Isabelle/Isar. |
|
49 |
|
50 * HOL/Isar_examples (Markus Wenzel) |
|
51 More examples, including a formulation of Hoare Logic in Isabelle/Isar. |
|
52 |
|
53 * HOL/Prolog (David von Oheimb) |
|
54 A (bare-bones) implementation of Lambda-Prolog. |
11 |
55 |
12 See the NEWS file distributed with Isabelle for more details. |
56 See the NEWS file distributed with Isabelle for more details. |
13 |
57 |
14 |
58 |
15 You may get Isabelle99-1 from any of the following mirror sites: |
59 You may get Isabelle99-1 from any of the following mirror sites: |
16 |
60 |
17 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
61 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
18 Munich (Germany) http://isabelle.in.tum.de/dist/ |
62 Munich (Germany) http://isabelle.in.tum.de/dist/ |
19 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/source.html |
63 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html |
20 Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/source.html |
64 Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html |