50 now limited to individual terms, instead of whole simultaneous |
50 now limited to individual terms, instead of whole simultaneous |
51 specifications as before. This greatly reduces the complexity of the |
51 specifications as before. This greatly reduces the complexity of the |
52 syntax module and improves flexibility by separating parsing and |
52 syntax module and improves flexibility by separating parsing and |
53 type-checking. INCOMPATIBILITY: additional type-constraints (explicit |
53 type-checking. INCOMPATIBILITY: additional type-constraints (explicit |
54 'fixes' etc.) are required in rare situations. |
54 'fixes' etc.) are required in rare situations. |
|
55 |
|
56 * Syntax: constants introduced by new-style packages ('definition', |
|
57 'abbreviation' etc.) are passed through the syntax module in |
|
58 ``authentic mode''. This means that associated mixfix annotations |
|
59 really stick to such constants, independently of potential name space |
|
60 ambiguities introduced later on. INCOMPATIBILITY: constants in parse |
|
61 trees are represented slightly differently, may need to adapt syntax |
|
62 translations accordingly. Use CONST marker in 'translations' and |
|
63 @{const_syntax} antiquotation in 'parse_translation' etc. |
55 |
64 |
56 * Legacy goal package: reduced interface to the bare minimum required |
65 * Legacy goal package: reduced interface to the bare minimum required |
57 to keep existing proof scripts running. Most other user-level |
66 to keep existing proof scripts running. Most other user-level |
58 functions are now part of the OldGoals structure, which is *not* open |
67 functions are now part of the OldGoals structure, which is *not* open |
59 by default (consider isatool expandshort before open OldGoals). |
68 by default (consider isatool expandshort before open OldGoals). |