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