equal
deleted
inserted
replaced
5 |
5 |
6 This release introduces fundamental changes over Isabelle2005, see the |
6 This release introduces fundamental changes over Isabelle2005, see the |
7 NEWS file in the distribution for more details. Numerous existing |
7 NEWS file in the distribution for more details. Numerous existing |
8 concepts have been generalized and re-implemented based on novel |
8 concepts have been generalized and re-implemented based on novel |
9 system architecture. New theories and proof tools have been added |
9 system architecture. New theories and proof tools have been added |
10 (mostly for HOL). |
10 (mostly for HOL). Some highlights are: |
11 |
|
12 The main highlights are: |
|
13 |
11 |
14 * Support for nominal datatypes (binding structures) due to the |
12 * Support for nominal datatypes (binding structures) due to the |
15 HOL-Nominal logic. |
13 HOL-Nominal logic. |
16 |
14 |
17 * General local theory infrastructure for specifications depending on |
15 * General local theory infrastructure for specifications depending on |
31 'sledgehammer' command for automated proof synthesis. |
29 'sledgehammer' command for automated proof synthesis. |
32 |
30 |
33 * Second generation code generator for a subset of HOL, targeting SML, |
31 * Second generation code generator for a subset of HOL, targeting SML, |
34 Haskell, and OCaml. |
32 Haskell, and OCaml. |
35 |
33 |
36 * Command 'normal_form' and method 'normalization' |
34 * Embedding of ML code into theories with static references to the |
37 for evaluating terms with free variables. |
35 logical context (via antiquotations). |
38 |
36 |
39 * Full list comprehension syntax. |
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. |
40 |
43 |
41 * Parallel loading of theories based on native multicore support in |
44 * Parallel loading of theories based on native multicore support in |
42 Poly/ML 5.1. |
45 Poly/ML 5.1. |
43 |
|
44 * Much improved algebraic capabilities, including Groebner bases. |
|
45 |
46 |
46 |
47 |
47 You may get Isabelle2007 from the following mirror sites: |
48 You may get Isabelle2007 from the following mirror sites: |
48 |
49 |
49 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |
50 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ |