--- 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 ***
--- 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)