equal
deleted
inserted
replaced
144 |
144 |
145 *** Isar *** |
145 *** Isar *** |
146 |
146 |
147 * Locales: |
147 * Locales: |
148 - "includes" disallowed in declaration of named locales (command "locale"). |
148 - "includes" disallowed in declaration of named locales (command "locale"). |
149 |
149 - Fixed parameter management in theorem generation for goals with "includes". |
|
150 INCOMPATIBILITY: rarely, the generated theorem statement is different. |
150 |
151 |
151 *** HOL *** |
152 *** HOL *** |
152 |
153 |
153 * HOL/record: reimplementation of records. Improved scalability for |
154 * HOL/record: reimplementation of records. Improved scalability for |
154 records with many fields, avoiding performance problems for type |
155 records with many fields, avoiding performance problems for type |