32 primes instead of base 26 numbers. |
32 primes instead of base 26 numbers. |
33 |
33 |
34 |
34 |
35 *** HOL *** |
35 *** HOL *** |
36 |
36 |
37 * HOL/record: reimplementation of records to avoid performance |
37 |
38 problems for type inference. Records are no longer composed of nested |
38 * HOL/record: reimplementation of records. Improved scalability for records with |
39 field types, but of nested extension types. Therefore the record type |
39 many fields, avoiding performance problems for type inference. Records are no |
40 only grows linear in the number of extensions and not in the number of |
40 longer composed of nested field types, |
41 fields. The top-level (users) view on records is preserved. |
41 but of nested extension types. Therefore the record type only grows |
|
42 linear in the number of extensions and not in the number of fields. |
|
43 The top-level (users) view on records is preserved. |
42 Potential INCOMPATIBILITY only in strange cases, where the theory |
44 Potential INCOMPATIBILITY only in strange cases, where the theory |
43 depends on the old record representation. The type generated for a |
45 depends on the old record representation. The type generated for |
44 record is called <record_name>_ext_type. |
46 a record is called <record_name>_ext_type. |
45 |
47 |
|
48 |
|
49 * Simplifier: "record_upd_simproc" for simplification of multiple record |
|
50 updates enabled by default. |
|
51 INCOMPATIBILITY: old proofs break occasionally, since simplification |
|
52 is more powerful by default. |
46 |
53 |
47 *** HOLCF *** |
54 *** HOLCF *** |
48 |
55 |
49 * HOLCF: discontinued special version of 'constdefs' (which used to |
56 * HOLCF: discontinued special version of 'constdefs' (which used to |
50 support continuous functions) in favor of the general Pure one with |
57 support continuous functions) in favor of the general Pure one with |