equal
deleted
inserted
replaced
276 |
276 |
277 * New (co)datatype package: |
277 * New (co)datatype package: |
278 - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF |
278 - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF |
279 structure on the raw type to an abstract type defined using typedef. |
279 structure on the raw type to an abstract type defined using typedef. |
280 - Always generate "case_transfer" theorem. |
280 - Always generate "case_transfer" theorem. |
|
281 |
|
282 * Transfer: |
|
283 - new methods for interactive debugging of 'transfer' and |
|
284 'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end', |
|
285 'transfer_prover_start' and 'transfer_prover_end'. |
281 |
286 |
282 * Division on integers is bootstrapped directly from division on |
287 * Division on integers is bootstrapped directly from division on |
283 naturals and uses generic numeral algorithm for computations. |
288 naturals and uses generic numeral algorithm for computations. |
284 Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes |
289 Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes |
285 former simprocs binary_int_div and binary_int_mod |
290 former simprocs binary_int_div and binary_int_mod |