1 Subject: Announcing Isabelle2005 |
1 Subject: Announcing Isabelle2007 |
2 To: isabelle-users@cl.cam.ac.uk |
2 To: isabelle-users@cl.cam.ac.uk |
3 |
3 |
4 Isabelle2005 is now available. |
4 Isabelle2007 is finally available. |
5 |
5 |
6 This release provides substantial advances over Isabelle2004, see the |
6 This release introduces fundamental changes over Isabelle2005, see the |
7 first 1000 lines of NEWS in the distribution for more details. Some |
7 NEWS file in the distribution for more details. Numerous existing |
8 highlights are: |
8 concepts have been generalized and re-implemented based on novel |
|
9 system architecture. New theories and proof tools have been added |
|
10 (mostly for HOL). |
9 |
11 |
10 * Interpretation of locale expressions in theories, locales, and proof |
12 The main highlights are: |
11 contexts. |
|
12 |
13 |
13 * Substantial library improvements (HOL, HOL-Complex, HOLCF). |
14 * New 'function' package for general recursive function definitions. |
14 |
15 |
15 * Proof tools for transitivity reasoning. |
16 * New version of 'inductive' package for inductive predicates; |
|
17 separate variant 'inductive_set'. |
16 |
18 |
17 * General 'find_theorems' command (by term patterns, as |
19 * New basic specification elements 'definition', 'axiomatization', |
18 intro/elim/simp rules etc.). |
20 'abbreviation', 'notation'. |
19 |
21 |
20 * Commands for generating ad-hoc draft documents. |
22 * New 'class' package combination of axclass + locale interpretation. |
21 |
23 |
22 * Support for Unicode proof documents (UTF-8). |
24 * Fully featured support for nominal datatypes (binding structures) |
|
25 due to the HOL-Nominal logic. |
23 |
26 |
24 * Major internal reorganizations and performance improvements. |
27 * Various improvements in locale infrastructure (interpretation etc.) |
|
28 |
|
29 * Various improvements of Isar language elements and related proof |
|
30 tools. |
|
31 |
|
32 * Built-in Metis prover, external linkup for automated provers, and |
|
33 'sledghammer' command for automated proof synthesis. |
|
34 |
|
35 * General local theory infrastructure for specifications depending on |
|
36 parameters and assumptions (e.g. from locales, classes). |
|
37 |
|
38 * Second generation code-generator for a subset of HOL, targeting SML, |
|
39 Haskell, and OCaml. |
|
40 |
|
41 * Improved support for arbitrary ML operations depending on the |
|
42 logical context. |
|
43 |
|
44 * Parallel loading of theories based on native multicore support in |
|
45 Poly/ML 5.1. |
25 |
46 |
26 |
47 |
27 You may get Isabelle2005 from the following mirror sites: |
48 You may get Isabelle2007 from the following mirror sites: |
28 |
49 |
29 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |
50 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |
30 Munich (Germany) http://isabelle.in.tum.de/ |
51 Munich (Germany) http://isabelle.in.tum.de/ |
31 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ |
52 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ |