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 


14 
The most prominent highlights of Isabelle991 are as follows.

9928

15 

10161

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.

10166

24 
o Extended "Isabelle/Isar Reference Manual".

9928

25 

10166

26 
* HOL/Algebra (Clemens Ballarin)


27 
Rings and univariate polynomials.

10161

28 

10162

29 
* HOL/BCV (Tobias Nipkow)


30 
Generic model of bytecode verification, i.e. dataflow


31 
analysis for assembly languages with subtypes.


32 

10166

33 
* HOL/IMPP (David von Oheimb)


34 
Extension of IMP with local variables and mutually recursive


35 
procedures.

10161

36 

10166

37 
* HOL/Isar_examples (Markus Wenzel)


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

10161

39 


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


41 
More on termination of simplytyped lambdaterms; converted into


42 
an Isabelle/Isar tactic emulation script.


43 


44 
* HOL/Lattice (Markus Wenzel)


45 
Lattices and orders in Isabelle/Isar.


46 

10166

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


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 

10161

57 
* HOL/Prolog (David von Oheimb)


58 
A (barebones) implementation of LambdaProlog.

9928

59 

10167

60 
* HOL/Real (Jacques Fleuriot)


61 
More on nonstandard real analysis.

10166

62 


63 

9928

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:


68 


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


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

10161

71 
New Jersey (USA) ftp://ftp.research.belllabs.com/dist/smlnj/isabelle/index.html


72 
Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html
