equal
deleted
inserted
replaced
575 |
575 |
576 * (Co)datatype package: |
576 * (Co)datatype package: |
577 - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF |
577 - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF |
578 structure on the raw type to an abstract type defined using typedef. |
578 structure on the raw type to an abstract type defined using typedef. |
579 - Always generate "case_transfer" theorem. |
579 - Always generate "case_transfer" theorem. |
|
580 - For mutual types, generate slightly stronger "rel_induct", "rel_coinduct", |
|
581 and "coinduct" theorems. INCOMPATIBLITY. |
580 - Allow discriminators and selectors with the same name as the type |
582 - Allow discriminators and selectors with the same name as the type |
581 being defined. |
583 being defined. |
582 - Avoid various internal name clashes (e.g., 'datatype f = f'). |
584 - Avoid various internal name clashes (e.g., 'datatype f = f'). |
583 |
585 |
584 * Transfer: new methods for interactive debugging of 'transfer' and |
586 * Transfer: new methods for interactive debugging of 'transfer' and |