|
nipkow@14021
|
1 |
Subject: Announcing Isabelle2003
|
|
wenzelm@9928
|
2 |
To: isabelle-users@cl.cam.ac.uk
|
|
wenzelm@9928
|
3 |
|
|
nipkow@14021
|
4 |
Isabelle2003 is now available.
|
|
wenzelm@12927
|
5 |
|
|
nipkow@14021
|
6 |
This release provides many improvements and a few substantial advances over
|
|
nipkow@14021
|
7 |
Isabelle2002. The most prominent highlights of Isabelle2003 are as follows
|
|
nipkow@14021
|
8 |
(see the NEWS of the distribution for more details):
|
|
wenzelm@12927
|
9 |
|
|
nipkow@14021
|
10 |
* New framework for extracting programs from constructive proofs in HOL.
|
|
nipkow@14021
|
11 |
(Berghofer)
|
|
wenzelm@9928
|
12 |
|
|
nipkow@14021
|
13 |
* Improved simplifier. The premises of a goal are completely
|
|
nipkow@14021
|
14 |
interreduced, ie simplified wrt each other. (Berghofer)
|
|
wenzelm@9928
|
15 |
|
|
nipkow@14021
|
16 |
* Presburger arithmetic. Method arith can deal with quantified formulae over
|
|
nipkow@14021
|
17 |
nat and int, and with mod, div and dvd wrt a numeral. (Chaieb and Nipkow)
|
|
wenzelm@10161
|
18 |
|
|
nipkow@14021
|
19 |
* New command to find all rules whose conclusion matches the current goal.
|
|
wenzelm@10161
|
20 |
|
|
nipkow@14021
|
21 |
* New command to trace why unification failed.
|
|
wenzelm@12964
|
22 |
|
|
nipkow@14021
|
23 |
* Locales (named proof contexts). The new implementation is fully
|
|
nipkow@14021
|
24 |
integrated with Isar's notion of proof context, and locale specifications
|
|
nipkow@14021
|
25 |
produce predicate definitions that allow to work with locales in more
|
|
nipkow@14021
|
26 |
flexible ways. (Wenzel)
|
|
wenzelm@12983
|
27 |
|
|
nipkow@14021
|
28 |
* HOL/Algebra: proofs in classical algebra. Intended as a base for all
|
|
nipkow@14021
|
29 |
algebraic developments in HOL. Currently covers group and ring theory.
|
|
nipkow@14021
|
30 |
(Ballarin, Kammüller, Paulson)
|
|
wenzelm@12983
|
31 |
|
|
nipkow@14021
|
32 |
* HOL/Complex defines the type "complex" of the complex numbers, with numeric
|
|
nipkow@14021
|
33 |
constants and some complex analysis, including nonstandard analysis. The
|
|
nipkow@14021
|
34 |
image HOL-Complex should be used for developments involving the real
|
|
nipkow@14021
|
35 |
numbers too. Gauge integration and hyperreal logarithms have recently
|
|
nipkow@14021
|
36 |
been added. (Fleuriot)
|
|
wenzelm@12983
|
37 |
|
|
nipkow@14021
|
38 |
* HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad,
|
|
nipkow@14021
|
39 |
Gray and Kramer)
|
|
wenzelm@12983
|
40 |
|
|
nipkow@14021
|
41 |
* ZF/Constructible: Gödel's proof of the relative consistency of the axiom
|
|
nipkow@14021
|
42 |
of choice is mechanized using Isabelle/ZF, following, Kunen's famous
|
|
nipkow@14021
|
43 |
textbook "Set Theory". (Paulson)
|
|
wenzelm@12983
|
44 |
|
|
nipkow@14021
|
45 |
You may get Isabelle2003 from any of the following mirror sites:
|
|
wenzelm@9928
|
46 |
|
|
wenzelm@9928
|
47 |
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
|
|
wenzelm@9928
|
48 |
Munich (Germany) http://isabelle.in.tum.de/dist/
|