equal
deleted
inserted
replaced
13 * Theory syntax: the old non-Isar theory file format has been |
13 * Theory syntax: the old non-Isar theory file format has been |
14 discontinued altogether. Note that ML proof scripts may still be used |
14 discontinued altogether. Note that ML proof scripts may still be used |
15 with Isar theories; migration is usually quite simple with the ML |
15 with Isar theories; migration is usually quite simple with the ML |
16 function use_legacy_bindings. INCOMPATIBILITY. |
16 function use_legacy_bindings. INCOMPATIBILITY. |
17 |
17 |
18 * Theory syntax: some popular names (e.g. "class", "if", "fun") are |
18 * Theory syntax: some popular names (e.g. "class", "fun", "help", |
19 now keywords. INCOMPATIBILITY, use double quotes. |
19 "if") are now keywords. INCOMPATIBILITY, use double quotes. |
20 |
20 |
21 * Legacy goal package: reduced interface to the bare minimum required |
21 * Legacy goal package: reduced interface to the bare minimum required |
22 to keep existing proof scripts running. Most other user-level |
22 to keep existing proof scripts running. Most other user-level |
23 functions are now part of the OldGoals structure, which is *not* open |
23 functions are now part of the OldGoals structure, which is *not* open |
24 by default (consider isatool expandshort before open OldGoals). |
24 by default (consider isatool expandshort before open OldGoals). |
52 * Added antiquotations @{ML_type text} and @{ML_struct text} which |
52 * Added antiquotations @{ML_type text} and @{ML_struct text} which |
53 check the given source text as ML type/structure, printing verbatim. |
53 check the given source text as ML type/structure, printing verbatim. |
54 |
54 |
55 * Added antiquotation @{abbrev "c args"} which prints the abbreviation |
55 * Added antiquotation @{abbrev "c args"} which prints the abbreviation |
56 "c args == rhs" given in the current context. (Any number of |
56 "c args == rhs" given in the current context. (Any number of |
57 arguments on the LHS may be given.) |
57 arguments may be given on the LHS.) |
58 |
58 |
59 |
59 |
60 |
60 |
61 *** Pure *** |
61 *** Pure *** |
62 |
62 |
284 |
284 |
285 Concrete syntax is attached to specified constants in internal form, |
285 Concrete syntax is attached to specified constants in internal form, |
286 independently of name spaces. The parse tree representation is |
286 independently of name spaces. The parse tree representation is |
287 slightly different -- use 'notation' instead of raw 'syntax', and |
287 slightly different -- use 'notation' instead of raw 'syntax', and |
288 'translations' with explicit "CONST" markup to accommodate this. |
288 'translations' with explicit "CONST" markup to accommodate this. |
|
289 |
|
290 * Pure: command 'print_abbrevs' prints all constant abbreviations of |
|
291 the current context. Print mode "no_abbrevs" prevents inversion of |
|
292 abbreviations on output. |
289 |
293 |
290 * Isar/locales: improved parameter handling: |
294 * Isar/locales: improved parameter handling: |
291 - use of locales "var" and "struct" no longer necessary; |
295 - use of locales "var" and "struct" no longer necessary; |
292 - parameter renamings are no longer required to be injective. |
296 - parameter renamings are no longer required to be injective. |
293 This enables, for example, to define a locale for endomorphisms thus: |
297 This enables, for example, to define a locale for endomorphisms thus: |