--- a/NEWS Sun Jan 24 12:21:57 2016 +0100
+++ b/NEWS Sun Jan 24 12:33:09 2016 +0100
@@ -594,8 +594,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.
+ - 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').
@@ -682,8 +682,8 @@
less_eq_multiset.rep_eq ~> subseteq_mset_def
INCOMPATIBILITY
- Removed lemmas generated by lift_definition:
- less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer
- less_eq_multiset_def
+ less_eq_multiset.abs_eq, less_eq_multiset.rsp,
+ less_eq_multiset.transfer, less_eq_multiset_def
INCOMPATIBILITY
* Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a.