1 
1 
2 Subject: Announcing Isabelle991 
2 Subject: Announcing Isabelle991 
3 To: isabelleusers@cl.cam.ac.uk 
3 To: isabelleusers@cl.cam.ac.uk 
4 
4 
5 Isabelle991 is now available. 
5 Isabelle991 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 Isabelle991 are as follows. 
9 
15 
10 * 
16 * Isabelle/Isar improvements (Markus Wenzel) 

17 o Support of tacticemulation 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 HindleyMilner polymorphism for proof texts. 

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

23 fake mathmode. 

24 o Extended "Isabelle/Isar Reference Manual" 

25 http://isabelle.in.tum.de/doc/isarref.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 typesafety. 

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 simplytyped lambdaterms; 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 (barebones) implementation of LambdaProlog. 
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 Isabelle991 from any of the following mirror sites: 
59 You may get Isabelle991 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.belllabs.com/dist/smlnj/isabelle/source.html 
63 New Jersey (USA) ftp://ftp.research.belllabs.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 