# HG changeset patch
# User wenzelm
# Date 1453635189 -3600
# Node ID 3687c199e22b361aa83db5c58ef78e590a3755bd
# Parent  7cc9d7b822ae73bec0d939dec08f1c43198a84b6
tuned;

diff -r 7cc9d7b822ae -r 3687c199e22b NEWS
--- 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.