--- a/NEWS Wed Jan 13 09:09:37 2016 +0100
+++ b/NEWS Wed Jan 13 09:09:38 2016 +0100
@@ -577,6 +577,8 @@
- New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
structure on the raw type to an abstract type defined using typedef.
- Always generate "case_transfer" theorem.
+ - For mutual types, generate slightly stronger "rel_induct", "rel_coinduct",
+ and "coinduct" theorems. INCOMPATIBLITY.
- Allow discriminators and selectors with the same name as the type
being defined.
- Avoid various internal name clashes (e.g., 'datatype f = f').