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