|
9928
|
1 |
|
|
12927
|
2 |
Subject: Announcing Isabelle2002
|
|
9928
|
3 |
To: isabelle-users@cl.cam.ac.uk
|
|
|
4 |
|
|
12927
|
5 |
Isabelle2002 is now available.
|
|
|
6 |
|
|
12995
|
7 |
This release provides major improvements. The Isar language has
|
|
|
8 |
reached a mature state; the core engine is able to record full proof
|
|
|
9 |
terms; many aspects of the library have been reworked; several
|
|
|
10 |
substantial case studies have been added. Some changes may cause
|
|
|
11 |
incompatibility with earlier versions, but improve accessibility of
|
|
|
12 |
Isabelle for new users.
|
|
12927
|
13 |
|
|
12983
|
14 |
The most prominent highlights of Isabelle2002 are as follows (see the
|
|
|
15 |
NEWS of the distribution for more details).
|
|
12964
|
16 |
|
|
12995
|
17 |
* The Isabelle/HOL tutorial is to be published as LNCS 2283;
|
|
12983
|
18 |
Isabelle2002 is the official version to go along with that book
|
|
|
19 |
(by Tobias Nipkow, Larry Paulson, Markus Wenzel).
|
|
|
20 |
|
|
|
21 |
* Pure: explicit proof terms for all internal inferences:
|
|
|
22 |
object-logics, proof tools etc. will benefit automatically
|
|
|
23 |
(by Stefan Berghofer).
|
|
10161
|
24 |
|
|
12983
|
25 |
* Pure/Isar: proper integration of the locale package for modular
|
|
|
26 |
theory development; additional support for rename/merge
|
|
|
27 |
operations, and type-inference for structured specifications
|
|
|
28 |
(by Markus Wenzel).
|
|
|
29 |
|
|
|
30 |
* Pure/Isar: streamlined induction proof patterns
|
|
|
31 |
(by Markus Wenzel).
|
|
|
32 |
|
|
|
33 |
* Pure/HOL: infrastructure for generating functional and relational
|
|
|
34 |
code, using the ML run-time environment (by Stefan Berghofer).
|
|
|
35 |
|
|
12993
|
36 |
* HOL/library: numerals on all number types; several
|
|
12983
|
37 |
improvements of tuple and record types; new definite description
|
|
12993
|
38 |
operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
|
|
12964
|
39 |
|
|
12983
|
40 |
* HOL/Bali: large application concerning formal treatment of Java.
|
|
|
41 |
(by David von Oheimb and Norbert Schirmer).
|
|
|
42 |
|
|
12996
|
43 |
* HOL/HoareParallel: large application concerning verification of
|
|
|
44 |
parallel imperative programs (Owicki-Gries method, Rely-Guarantee
|
|
12999
|
45 |
method, including examples of garbage collection, mutual
|
|
12996
|
46 |
exclusion, etc.)
|
|
12983
|
47 |
(by Leonor Prensa Nieto).
|
|
|
48 |
|
|
|
49 |
* HOL/GroupTheory: group theory examples including Sylow's theorem
|
|
|
50 |
(by Florian Kammüller).
|
|
9928
|
51 |
|
|
12983
|
52 |
* HOL/IMP: new proofs in Isar format
|
|
|
53 |
(by Gerwin Klein).
|
|
|
54 |
|
|
13007
|
55 |
* HOL/MicroJava: exception handling on the bytecode level
|
|
|
56 |
(by Gerwin Klein).
|
|
|
57 |
|
|
12983
|
58 |
* ZF/UNITY: typeless version of Chandy and Misra's formalism
|
|
|
59 |
(by Sidi O Ehmety).
|
|
10162
|
60 |
|
|
12983
|
61 |
* System: improvements and simplifications of document preparation
|
|
|
62 |
(by Markus Wenzel).
|
|
|
63 |
|
|
|
64 |
* System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
|
|
|
65 |
larger heap size of applications.
|
|
|
66 |
|
|
|
67 |
* System: support for MacOS X (for Poly/ML and SML/NJ).
|
|
12964
|
68 |
|
|
10166
|
69 |
|
|
12964
|
70 |
You may get Isabelle2002 from any of the following mirror sites:
|
|
9928
|
71 |
|
|
|
72 |
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
|
|
|
73 |
Munich (Germany) http://isabelle.in.tum.de/dist/
|
|
10161
|
74 |
New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
|
|
|
75 |
Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html
|