9928

1 


2 
Subject: Announcing Isabelle991


3 
To: isabelleusers@cl.cam.ac.uk


4 

10161

5 
Isabelle991 is now available. This release continues the line of


6 
Isabelle99, introducing numerous improvements, both internal and user


7 
visible.


8 


9 
In particular, great care has been taken to improve robustness and


10 
ease use and installation of the complete Isabelle working

10165

11 
environment. This includes Proof General user interface support, WWW

10161

12 
presentation of theories and the Isabelle document preparation system.


13 

10168

14 
The most prominent highlights of Isabelle991 are as follows. See the


15 
NEWS file distributed with Isabelle for more details.

9928

16 

10161

17 
* Isabelle/Isar improvements (Markus Wenzel)


18 
o Support of tacticemulation scripts for easy porting of legacy ML


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.

10166

25 
o Extended "Isabelle/Isar Reference Manual".

9928

26 

10166

27 
* HOL/Algebra (Clemens Ballarin)


28 
Rings and univariate polynomials.

10161

29 

10162

30 
* HOL/BCV (Tobias Nipkow)

10168

31 
Generic model of bytecode verification.

10162

32 

10166

33 
* HOL/IMPP (David von Oheimb)

10168

34 
Extension of IMP with local variables and mutually recursive procedures.

10161

35 

10166

36 
* HOL/Isar_examples (Markus Wenzel)


37 
More examples, including a formulation of Hoare Logic in Isabelle/Isar.

10161

38 


39 
* HOL/Lambda (Stefan Berghofer and Tobias Nipkow)

10168

40 
More on termination of simplytyped lambdaterms (Isar script).

10161

41 


42 
* HOL/Lattice (Markus Wenzel)


43 
Lattices and orders in Isabelle/Isar.


44 

10166

45 
* HOL/MicroJava (Gerwin Klein, Tobias Nipkow, David von Oheimb, and


46 
Cornelia Pusch)


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

10168

48 
virtual machine and a specification of its bytecode verifier.

10166

49 


50 
* HOL/NumberTheory (Thomas Rasmussen)


51 
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem,


52 
Fermat/Euler Theorem, Wilson's Theorem.


53 

10161

54 
* HOL/Prolog (David von Oheimb)


55 
A (barebones) implementation of LambdaProlog.

9928

56 

10167

57 
* HOL/Real (Jacques Fleuriot)


58 
More on nonstandard real analysis.

10166

59 

9928

60 
You may get Isabelle991 from any of the following mirror sites:


61 


62 
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/


63 
Munich (Germany) http://isabelle.in.tum.de/dist/

10161

64 
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
