9 In particular, great care has been taken to improve robustness and |
9 In particular, great care has been taken to improve robustness and |
10 ease use and installation of the complete Isabelle working |
10 ease use and installation of the complete Isabelle working |
11 environment. This includes Proof General user interface support, WWW |
11 environment. This includes Proof General user interface support, WWW |
12 presentation of theories and the Isabelle document preparation system. |
12 presentation of theories and the Isabelle document preparation system. |
13 |
13 |
14 The most prominent highlights of Isabelle99-1 are as follows. |
14 The most prominent highlights of Isabelle99-1 are as follows. See the |
|
15 NEWS file distributed with Isabelle for more details. |
15 |
16 |
16 * Isabelle/Isar improvements (Markus Wenzel) |
17 * Isabelle/Isar improvements (Markus Wenzel) |
17 o Support of tactic-emulation scripts for easy porting of legacy ML |
18 o Support of tactic-emulation scripts for easy porting of legacy ML |
18 scripts (see also the HOL/Lambda example). |
19 scripts (see also the HOL/Lambda example). |
19 o Better support for scalable verification tasks (manage large |
20 o Better support for scalable verification tasks (manage large |
25 |
26 |
26 * HOL/Algebra (Clemens Ballarin) |
27 * HOL/Algebra (Clemens Ballarin) |
27 Rings and univariate polynomials. |
28 Rings and univariate polynomials. |
28 |
29 |
29 * HOL/BCV (Tobias Nipkow) |
30 * HOL/BCV (Tobias Nipkow) |
30 Generic model of bytecode verification, i.e. data-flow |
31 Generic model of bytecode verification. |
31 analysis for assembly languages with subtypes. |
|
32 |
32 |
33 * HOL/IMPP (David von Oheimb) |
33 * HOL/IMPP (David von Oheimb) |
34 Extension of IMP with local variables and mutually recursive |
34 Extension of IMP with local variables and mutually recursive procedures. |
35 procedures. |
|
36 |
35 |
37 * HOL/Isar_examples (Markus Wenzel) |
36 * HOL/Isar_examples (Markus Wenzel) |
38 More examples, including a formulation of Hoare Logic in Isabelle/Isar. |
37 More examples, including a formulation of Hoare Logic in Isabelle/Isar. |
39 |
38 |
40 * HOL/Lambda (Stefan Berghofer and Tobias Nipkow) |
39 * HOL/Lambda (Stefan Berghofer and Tobias Nipkow) |
41 More on termination of simply-typed lambda-terms; converted into |
40 More on termination of simply-typed lambda-terms (Isar script). |
42 an Isabelle/Isar tactic emulation script. |
|
43 |
41 |
44 * HOL/Lattice (Markus Wenzel) |
42 * HOL/Lattice (Markus Wenzel) |
45 Lattices and orders in Isabelle/Isar. |
43 Lattices and orders in Isabelle/Isar. |
46 |
44 |
47 * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and |
45 * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and |
48 Cornelia Pusch) |
46 Cornelia Pusch) |
49 Formalization of a fragment of Java, together with a corresponding |
47 Formalization of a fragment of Java, together with a corresponding |
50 virtual machine and a specification of its bytecode verifier and a |
48 virtual machine and a specification of its bytecode verifier. |
51 lightweight bytecode verifier, including proofs of type-safety. |
|
52 |
49 |
53 * HOL/NumberTheory (Thomas Rasmussen) |
50 * HOL/NumberTheory (Thomas Rasmussen) |
54 Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, |
51 Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, |
55 Fermat/Euler Theorem, Wilson's Theorem. |
52 Fermat/Euler Theorem, Wilson's Theorem. |
56 |
53 |
58 A (bare-bones) implementation of Lambda-Prolog. |
55 A (bare-bones) implementation of Lambda-Prolog. |
59 |
56 |
60 * HOL/Real (Jacques Fleuriot) |
57 * HOL/Real (Jacques Fleuriot) |
61 More on nonstandard real analysis. |
58 More on nonstandard real analysis. |
62 |
59 |
63 |
|
64 See the NEWS file distributed with Isabelle for more details. |
|
65 |
|
66 |
|
67 You may get Isabelle99-1 from any of the following mirror sites: |
60 You may get Isabelle99-1 from any of the following mirror sites: |
68 |
61 |
69 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
62 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
70 Munich (Germany) http://isabelle.in.tum.de/dist/ |
63 Munich (Germany) http://isabelle.in.tum.de/dist/ |
71 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html |
64 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html |