equal
deleted
inserted
replaced
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). |
11 |
11 |
12 The main highlights are: |
12 The main highlights are: |
13 |
13 |
14 * Fully featured support for nominal datatypes (binding structures) |
14 * Support for nominal datatypes (binding structures) due to the |
15 due to the HOL-Nominal logic. |
15 HOL-Nominal logic. |
16 |
16 |
17 * General local theory infrastructure for specifications depending on |
17 * General local theory infrastructure for specifications depending on |
18 parameters and assumptions (e.g. from locales, classes). |
18 parameters and assumptions (e.g. from locales, classes). |
19 |
19 |
20 * New basic specification elements 'definition', 'axiomatization', |
20 * New basic specification elements 'definition', 'axiomatization', |