equal
deleted
inserted
replaced
93 linear in the number of extensions and not in the number of fields. |
93 linear in the number of extensions and not in the number of fields. |
94 The top-level (users) view on records is preserved. Potential |
94 The top-level (users) view on records is preserved. Potential |
95 INCOMPATIBILITY only in strange cases, where the theory depends on |
95 INCOMPATIBILITY only in strange cases, where the theory depends on |
96 the old record representation. The type generated for a record is |
96 the old record representation. The type generated for a record is |
97 called <record_name>_ext_type. |
97 called <record_name>_ext_type. |
|
98 |
|
99 * HOL/record: Reference record_definition_quick_and_dirty_sensitive |
|
100 can be enabled to skip the proofs triggered by a record definition |
|
101 (if quick_and_dirty is enabled). Definitions of large records can |
|
102 take quite long. |
98 |
103 |
99 * HOL: symbolic syntax of Hilbert Choice Operator is now as follows: |
104 * HOL: symbolic syntax of Hilbert Choice Operator is now as follows: |
100 |
105 |
101 syntax (epsilon) |
106 syntax (epsilon) |
102 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) |
107 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) |