21 function use_legacy_bindings. INCOMPATIBILITY. |
21 function use_legacy_bindings. INCOMPATIBILITY. |
22 |
22 |
23 * Theory syntax: some popular names (e.g. 'class', 'declaration', |
23 * Theory syntax: some popular names (e.g. 'class', 'declaration', |
24 'fun', 'help', 'if') are now keywords. INCOMPATIBILITY, use double |
24 'fun', 'help', 'if') are now keywords. INCOMPATIBILITY, use double |
25 quotes. |
25 quotes. |
|
26 |
|
27 * Theory loader: be more serious about observing the static theory |
|
28 header specifications (including optional directories), but not the |
|
29 accidental file locations of previously successful loads. Potential |
|
30 INCOMPATIBILITY, may need to refine theory headers. |
|
31 |
|
32 * Theory loader: optional support for content-based file |
|
33 identification, instead of the traditional scheme of full physical |
|
34 path plus date stamp; configured by the ISABELLE_FILE_IDENT setting, |
|
35 (cf. the system manual). The new scheme allows to work with |
|
36 non-finished theories in persistent session images, such that source |
|
37 files may be moved later on without requiring reloads. |
26 |
38 |
27 * Legacy goal package: reduced interface to the bare minimum required |
39 * Legacy goal package: reduced interface to the bare minimum required |
28 to keep existing proof scripts running. Most other user-level |
40 to keep existing proof scripts running. Most other user-level |
29 functions are now part of the OldGoals structure, which is *not* open |
41 functions are now part of the OldGoals structure, which is *not* open |
30 by default (consider isatool expandshort before open OldGoals). |
42 by default (consider isatool expandshort before open OldGoals). |