2 Subject: Announcing Isabelle2002 |
2 Subject: Announcing Isabelle2002 |
3 To: isabelle-users@cl.cam.ac.uk |
3 To: isabelle-users@cl.cam.ac.uk |
4 |
4 |
5 Isabelle2002 is now available. |
5 Isabelle2002 is now available. |
6 |
6 |
7 This release provides major improvements. The Isar language has reached a |
7 This release provides major improvements. The Isar language has |
8 mature state; the treatment of numerals has been streamlined; several |
8 reached a mature state; the core engine is able to record full proof |
9 substantial case studies have been added. This occasionally causes |
9 terms; many aspects of the library have been reworked; several |
10 incompatibility with earlier versions. |
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. |
11 |
13 |
12 The most prominent highlights of Isabelle2002 are as follows (see the |
14 The most prominent highlights of Isabelle2002 are as follows (see the |
13 NEWS of the distribution for more details). |
15 NEWS of the distribution for more details). |
14 |
16 |
15 * The Isabelle/HOL tutorial has been published as LNCS 2283; |
17 * The Isabelle/HOL tutorial is to be published as LNCS 2283; |
16 Isabelle2002 is the official version to go along with that book |
18 Isabelle2002 is the official version to go along with that book |
17 (by Tobias Nipkow, Larry Paulson, Markus Wenzel). |
19 (by Tobias Nipkow, Larry Paulson, Markus Wenzel). |
18 |
20 |
19 * Pure: explicit proof terms for all internal inferences: |
21 * Pure: explicit proof terms for all internal inferences: |
20 object-logics, proof tools etc. will benefit automatically |
22 object-logics, proof tools etc. will benefit automatically |