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 Isabelle991 are as follows. 
14 The most prominent highlights of Isabelle991 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 tacticemulation scripts for easy porting of legacy ML 
18 o Support of tacticemulation 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. dataflow 
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 simplytyped lambdaterms; converted into 
40 More on termination of simplytyped lambdaterms (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 typesafety. 

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 (barebones) implementation of LambdaProlog. 
55 A (barebones) implementation of LambdaProlog. 
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 Isabelle991 from any of the following mirror sites: 
60 You may get Isabelle991 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.belllabs.com/dist/smlnj/isabelle/index.html 
64 New Jersey (USA) ftp://ftp.research.belllabs.com/dist/smlnj/isabelle/index.html 