NEWS

--- a/NEWS	Sun Feb 28 20:13:07 2021 +0000
+++ b/NEWS	Mon Mar 01 08:16:22 2021 +0100
@@ -19,7 +19,11 @@
 corrected. Minor INCOMPATIBILITY.
 
 * Theory "Permutation" in HOL-Library has been renamed to the more
-specific "List_Permutation".
+specific "List_Permutation".  Note that most notions from that
+theory are already present in theory "Permutations".  INCOMPATIBILITY.
+
+* Lemma "permutes_induct" has been given named premised.
+INCOMPATIBILITY.
 
 
 *** ML ***