|
9928
|
1 |
|
|
12927
|
2 |
Subject: Announcing Isabelle2002
|
|
9928
|
3 |
To: isabelle-users@cl.cam.ac.uk
|
|
|
4 |
|
|
12927
|
5 |
Isabelle2002 is now available.
|
|
|
6 |
|
|
12964
|
7 |
In this release many important aspects of Isabelle have been reworked
|
|
|
8 |
to improve robustness and usability (this occasionally causes
|
|
|
9 |
incompatibility with earlier versions).
|
|
12927
|
10 |
|
|
12964
|
11 |
The most prominent highlights of Isabelle2002 are as follows; see the
|
|
|
12 |
NEWS of the distribution for more details.
|
|
|
13 |
|
|
|
14 |
* The Isabelle/HOL tutorial has been published as LNCS 2283;
|
|
|
15 |
Isabelle2002 is the official version to go along with that book.
|
|
10161
|
16 |
|
|
12964
|
17 |
* Explicit proof terms for Isabelle/Pure (Stefan Berghofer);
|
|
|
18 |
all object-logics, proof tools etc. will automatically benefit.
|
|
|
19 |
|
|
|
20 |
* Interation of locales
|
|
9928
|
21 |
|
|
12964
|
22 |
* Specific support for Poly/ML 4.1.1 and PolyML/4.1.2
|
|
|
23 |
(manage larger heaps, slightly faster).
|
|
10162
|
24 |
|
|
12964
|
25 |
|
|
10166
|
26 |
|
|
12964
|
27 |
You may get Isabelle2002 from any of the following mirror sites:
|
|
9928
|
28 |
|
|
|
29 |
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
|
|
|
30 |
Munich (Germany) http://isabelle.in.tum.de/dist/
|
|
10161
|
31 |
New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
|
|
|
32 |
Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html
|