13 to observe strictly sequential dependencies of definitions within a |
13 to observe strictly sequential dependencies of definitions within a |
14 single 'constdefs' section; moreover, the declared name needs to be an |
14 single 'constdefs' section; moreover, the declared name needs to be an |
15 identifier. If all fails, consider to fall back on 'consts' and |
15 identifier. If all fails, consider to fall back on 'consts' and |
16 'defs' separately. |
16 'defs' separately. |
17 |
17 |
18 * Pure: 'advanced' translation functions (parse_translation etc.) may |
|
19 depend on the signature of the theory context being presently used for |
|
20 parsing/printing, see also isar-ref manual. |
|
21 |
|
22 |
|
23 * Pure: improved indexed syntax and implicit structures. First of |
18 * Pure: improved indexed syntax and implicit structures. First of |
24 all, indexed syntax provides a notational device for subscripted |
19 all, indexed syntax provides a notational device for subscripted |
25 application, using the new syntax \<^bsub>term\<^esub> for arbitrary |
20 application, using the new syntax \<^bsub>term\<^esub> for arbitrary |
26 expressions. Secondly, in a local context with structure |
21 expressions. Secondly, in a local context with structure |
27 declarations, number indexes \<^sub>n or the empty index (default |
22 declarations, number indexes \<^sub>n or the empty index (default |
28 number 1) refer to a certain fixed variable implicitly. Typical |
23 number 1) refer to a certain fixed variable implicitly; option |
|
24 show_structs controls printing of implicit structures. Typical |
29 applications of these concepts involve record types and locales. |
25 applications of these concepts involve record types and locales. |
|
26 |
|
27 * Pure: 'advanced' translation functions (parse_translation etc.) may |
|
28 depend on the signature of the theory context being presently used for |
|
29 parsing/printing, see also isar-ref manual. |
30 |
30 |
31 * Pure: tuned internal renaming of symbolic identifiers -- attach |
31 * Pure: tuned internal renaming of symbolic identifiers -- attach |
32 primes instead of base 26 numbers. |
32 primes instead of base 26 numbers. |
33 |
33 |
|
34 |
34 *** HOL *** |
35 *** HOL *** |
35 |
36 |
36 * Records: |
37 * HOL/record: reimplementation of records to avoid performance |
37 Reimplementation of records to avoid performance problems for |
38 problems for type inference. Records are no longer composed of nested |
38 type inference. Records are no longer composed of nested field types, |
39 field types, but of nested extension types. Therefore the record type |
39 but of nested extension types. Therefore the record type only grows |
40 only grows linear in the number of extensions and not in the number of |
40 linear in the number of extensions and not in the number of fields. |
41 fields. The top-level (users) view on records is preserved. |
41 The top-level (users) view on records is preserved. |
42 Potential INCOMPATIBILITY only in strange cases, where the theory |
42 Potential INCOMPATIBILITY only in strange cases, where the theory |
43 depends on the old record representation. The type generated for a |
43 depends on the old record representation. The type generated for |
44 record is called <record_name>_ext_type. |
44 a record is called <record_name>_ext_type. |
45 |
45 |
46 |
46 *** HOLCF *** |
47 *** HOLCF *** |
47 |
48 |
48 * HOLCF: discontinued special version of 'constdefs' (which used to |
49 * HOLCF: discontinued special version of 'constdefs' (which used to |
49 support continuous functions) in favor of the general Pure one with |
50 support continuous functions) in favor of the general Pure one with |