# HG changeset patch
# User haftmann
# Date 1614582982 -3600
# Node ID 2aef2de6b17cb8f71f8e9bebfdb7bb6854b7a658
# Parent  ff24fe85ee5743a10157ec565d8f7dd4d55a1fa8
NEWS

diff -r ff24fe85ee57 -r 2aef2de6b17c 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 ***
diff -r ff24fe85ee57 -r 2aef2de6b17c src/HOL/Library/List_Permutation.thy
--- a/src/HOL/Library/List_Permutation.thy	Sun Feb 28 20:13:07 2021 +0000
+++ b/src/HOL/Library/List_Permutation.thy	Mon Mar 01 08:16:22 2021 +0100
@@ -8,6 +8,12 @@
 imports Permutations
 begin
 
+text \<open>
+  Note that multisets already provide the notion of permutated list and hence
+  this theory mostly echoes material already logically present in theory
+  \<^text>\<open>Permutations\<close>; it should be seldom needed.
+\<close>
+
 subsection \<open>An inductive definition \ldots\<close>
 
 inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixr \<open><~~>\<close> 50)