2 Subject: Announcing Isabelle99-2
3 To: isabelle-users@cl.cam.ac.uk
5 Isabelle99-2 is now available. This release continues the line of
6 Isabelle99, introducing various improvements in robustness and
9 The most prominent highlights of Isabelle99-2 are as follows. See the
10 NEWS file distributed with Isabelle for more details.
12 * Poly/ML 4.0 used by default
13 More robust, less disk space required.
15 * Simplifier (Stefan Berghofer)
16 Proper implementation as a derived rule, outside the kernel!
18 * Improved document preparation (Markus Wenzel)
19 Near math-mode, sub/super scripts, more symbols etc.
21 * Isabelle/Isar (Markus Wenzel)
22 Numerous usability improvements, e.g. support for initial
23 schematic goals, failure prediction of subgoal statements,
24 handling of non-atomic statements in induction.
26 * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
27 Thomas M Rasmussen, Markus Wenzel)
28 A collection of generic theories to be used together with main HOL.
30 * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson)
31 General cleanup, more on nonstandard real analysis.
33 * HOL/Unix (Markus Wenzel)
34 Some Aspects of Unix file-system security; demonstrates
35 Isabelle/Isar in typical system modelling and verification tasks.
37 * HOL/Tutorial (Tobias Nipkow, Lawrence C Paulson)
38 Extended version of the Isabelle/HOL tutorial.
40 You may get Isabelle99-2 from any of the following mirror sites:
42 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
43 Munich (Germany) http://isabelle.in.tum.de/dist/
44 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
45 Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html