1 Subject: Announcing Isabelle2007 |
1 Subject: Announcing Isabelle2008 |
2 To: isabelle-users@cl.cam.ac.uk |
2 To: isabelle-users@cl.cam.ac.uk |
3 |
3 |
4 Isabelle2007 is finally available. |
4 Isabelle2008 is now available. |
5 |
5 |
6 This release introduces fundamental changes over Isabelle2005, see the |
6 This release mostly consolidates Isabelle2007, see the NEWS file in |
7 NEWS file in the distribution for more details. Numerous existing |
7 the distribution for more details. Some notable improvements 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). Some highlights are: |
|
11 |
8 |
12 * Support for nominal datatypes (binding structures) due to the |
9 * ... |
13 HOL-Nominal logic. |
|
14 |
|
15 * General local theory infrastructure for specifications depending on |
|
16 parameters and assumptions (e.g. from locales, classes). |
|
17 |
|
18 * New basic specification elements 'definition', 'axiomatization', |
|
19 'abbreviation', 'notation'. |
|
20 |
|
21 * New version of 'inductive' package for inductive predicates; |
|
22 separate variant 'inductive_set'. |
|
23 |
|
24 * New 'function' package for general recursive function definitions. |
|
25 |
|
26 * New 'class' package combination of axclass + locale interpretation. |
|
27 |
|
28 * Built-in Metis prover, external linkup for automated provers, and |
|
29 'sledgehammer' command for automated proof synthesis. |
|
30 |
|
31 * Auto quickcheck: toplevel goals are tested for counterexamples |
|
32 automatically when they are stated. |
|
33 |
|
34 * Second generation code generator for a subset of HOL, targeting SML, |
|
35 Haskell, and OCaml. |
|
36 |
|
37 * Command 'normal_form' and method "normalization" for evaluating |
|
38 terms with free variables. |
|
39 |
|
40 * Full list comprehension syntax for HOL. |
|
41 |
|
42 * Much improved algebraic capabilities, including Groebner bases. |
|
43 |
|
44 * Embedding of ML code into theories with static references to the |
|
45 logical context (via antiquotations). |
|
46 |
|
47 * Parallel loading of theories based on native multicore support in |
|
48 Poly/ML 5.1. |
|
49 |
10 |
50 |
11 |
51 You may get Isabelle2007 from the following mirror sites: |
12 You may get Isabelle2008 from the following mirror sites: |
52 |
13 |
53 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |
14 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |
54 Munich (Germany) http://isabelle.in.tum.de/ |
15 Munich (Germany) http://isabelle.in.tum.de/ |
55 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ |
16 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ |