1 
1 
2 Subject: Announcing Isabelle991 
2 Subject: Announcing Isabelle992 
3 To: isabelleusers@cl.cam.ac.uk 
3 To: isabelleusers@cl.cam.ac.uk 
4 
4 
5 Isabelle991 is now available. This release continues the line of 
5 Isabelle992 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 Isabelle992 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 Isabelle991 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 tacticemulation 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 HindleyMilner polymorphism for proof texts. 

23 o More robust document preparation, better LaTeX output due to 

24 fake mathmode. 

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 nonatomic 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 mathmode, 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 simplytyped lambdaterms (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 filesystem 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 Isabelle992 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 (barebones) implementation of LambdaProlog. 

56 

57 * HOL/Real (Jacques Fleuriot) 

58 More on nonstandard real analysis. 

59 

60 You may get Isabelle991 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.belllabs.com/dist/smlnj/isabelle/index.html 
44 New Jersey (USA) ftp://ftp.research.belllabs.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 