NEWS
changeset 62159 56d35d0fda5b
parent 62157 adcaaf6c9910
child 62163 f25408289842
     1.1 --- a/NEWS	Wed Jan 13 09:09:37 2016 +0100
     1.2 +++ b/NEWS	Wed Jan 13 09:09:38 2016 +0100
     1.3 @@ -577,6 +577,8 @@
     1.4    - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
     1.5      structure on the raw type to an abstract type defined using typedef.
     1.6    - Always generate "case_transfer" theorem.
     1.7 +  - For mutual types, generate slightly stronger "rel_induct", "rel_coinduct",
     1.8 +    and "coinduct" theorems. INCOMPATIBLITY.
     1.9    - Allow discriminators and selectors with the same name as the type
    1.10      being defined.
    1.11    - Avoid various internal name clashes (e.g., 'datatype f = f').