214 rel_sum (using inductive). |
214 rel_sum (using inductive). |
215 INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead |
215 INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead |
216 of rel_prod_def and rel_sum_def. |
216 of rel_prod_def and rel_sum_def. |
217 Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names |
217 Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names |
218 changed (e.g. map_prod_transfer ~> prod.map_transfer). |
218 changed (e.g. map_prod_transfer ~> prod.map_transfer). |
219 - Parametricity theorems for map functions, relators, set |
219 - Parametricity theorems for map functions, relators, set functions, |
220 functions, constructors, case combinators, discriminators, |
220 constructors, case combinators, discriminators, selectors and |
221 selectors and (co)recursors are automatically proved and registred |
221 (co)recursors are automatically proved and registered as transfer |
222 as transfer rules. |
222 rules. |
223 |
|
224 |
223 |
225 * Old datatype package: |
224 * Old datatype package: |
226 - The old 'datatype' command has been renamed 'old_datatype', and |
225 - The old 'datatype' command has been renamed 'old_datatype', and |
227 'rep_datatype' has been renamed 'old_rep_datatype'. They are |
226 'rep_datatype' has been renamed 'old_rep_datatype'. They are |
228 provided by "~~/src/HOL/Library/Old_Datatype.thy". See |
227 provided by "~~/src/HOL/Library/Old_Datatype.thy". See |
264 - New option 'smt_reconstruction_step_timeout' to limit the |
263 - New option 'smt_reconstruction_step_timeout' to limit the |
265 reconstruction time of Z3 proof steps in the new 'smt' method. |
264 reconstruction time of Z3 proof steps in the new 'smt' method. |
266 - New option 'smt_statistics' to display statistics of the new 'smt' |
265 - New option 'smt_statistics' to display statistics of the new 'smt' |
267 method, especially runtime statistics of Z3 proof reconstruction. |
266 method, especially runtime statistics of Z3 proof reconstruction. |
268 |
267 |
269 * Lifting |
268 * Lifting: command 'lift_definition' allows to execute lifted constants |
270 - lift_definition command implements a workaround that allows us |
269 that have as a return type a datatype containing a subtype. This |
271 to execute lifted constants that have as a return type |
270 overcomes long-time limitations in the area of code generation and |
272 a datatype containing a subtype. |
271 lifting, and avoids tedious workarounds. |
273 This was a long time limitation in the area of code generation and |
|
274 lifting and the used workarounds were tedious. |
|
275 |
272 |
276 * Command and antiquotation "value" provide different evaluation slots |
273 * Command and antiquotation "value" provide different evaluation slots |
277 (again), where the previous strategy (NBE after ML) serves as default. |
274 (again), where the previous strategy (NBE after ML) serves as default. |
278 Minor INCOMPATIBILITY. |
275 Minor INCOMPATIBILITY. |
279 |
276 |