19 o Better support for scalable verification tasks (manage large 
19 o Better support for scalable verification tasks (manage large 
20 contexts in induction, generalized existence reasoning etc.) 
20 contexts in induction, generalized existence reasoning etc.) 
21 o HindleyMilner polymorphism for proof texts. 
21 o HindleyMilner polymorphism for proof texts. 
22 o More robust document preparation, better LaTeX output due to 
22 o More robust document preparation, better LaTeX output due to 
23 fake mathmode. 
23 fake mathmode. 
24 o Extended "Isabelle/Isar Reference Manual" 
24 o Extended "Isabelle/Isar Reference Manual". 
25 
25 
26 * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and 
26 * HOL/Algebra (Clemens Ballarin) 
27 Cornelia Pusch) 
27 Rings and univariate polynomials. 
28 Formalization of a fragment of Java, together with a corresponding 

29 virtual machine and a specification of its bytecode verifier and a 

30 lightweight bytecode verifier, including proofs of typesafety. 

31 
28 
32 * HOL/BCV (Tobias Nipkow) 
29 * HOL/BCV (Tobias Nipkow) 
33 Generic model of bytecode verification, i.e. dataflow 
30 Generic model of bytecode verification, i.e. dataflow 
34 analysis for assembly languages with subtypes. 
31 analysis for assembly languages with subtypes. 
35 
32 
36 * HOL/Real (Jacques Fleuriot) 
33 * HOL/IMPP (David von Oheimb) 
37 More on nonstandard real analysis. 
34 Extension of IMP with local variables and mutually recursive 

35 procedures. 
38 
36 
39 * HOL/Algebra (Clemens Ballarin) 
37 * HOL/Isar_examples (Markus Wenzel) 
40 Rings and univariate polynomials. 
38 More examples, including a formulation of Hoare Logic in Isabelle/Isar. 
41 

42 * HOL/NumberTheory (Thomas Rasmussen) 

43 Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, 

44 Fermat/Euler Theorem, Wilson's Theorem. 

45 
39 
46 * HOL/Lambda (Stefan Berghofer and Tobias Nipkow) 
40 * HOL/Lambda (Stefan Berghofer and Tobias Nipkow) 
47 More on termination of simplytyped lambdaterms; converted into 
41 More on termination of simplytyped lambdaterms; converted into 
48 an Isabelle/Isar tactic emulation script. 
42 an Isabelle/Isar tactic emulation script. 
49 
43 
50 * HOL/Lattice (Markus Wenzel) 
44 * HOL/Lattice (Markus Wenzel) 
51 Lattices and orders in Isabelle/Isar. 
45 Lattices and orders in Isabelle/Isar. 
52 
46 
53 * HOL/Isar_examples (Markus Wenzel) 
47 * HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and 
54 More examples, including a formulation of Hoare Logic in Isabelle/Isar. 
48 Cornelia Pusch) 

49 Formalization of a fragment of Java, together with a corresponding 

50 virtual machine and a specification of its bytecode verifier and a 

51 lightweight bytecode verifier, including proofs of typesafety. 

52 

53 * HOL/NumberTheory (Thomas Rasmussen) 

54 Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, 

55 Fermat/Euler Theorem, Wilson's Theorem. 

56 

57 * HOL/Real (Jacques Fleuriot) 

58 More on nonstandard real analysis. 
55 
59 
56 * HOL/Prolog (David von Oheimb) 
60 * HOL/Prolog (David von Oheimb) 
57 A (barebones) implementation of LambdaProlog. 
61 A (barebones) implementation of LambdaProlog. 

62 

63 
58 
64 
59 See the NEWS file distributed with Isabelle for more details. 
65 See the NEWS file distributed with Isabelle for more details. 
60 
66 
61 
67 
62 You may get Isabelle991 from any of the following mirror sites: 
68 You may get Isabelle991 from any of the following mirror sites: 