NEWS
authorhaftmann
Mon, 01 Mar 2021 08:16:22 +0100
changeset 73576 2aef2de6b17c
parent 73575 ff24fe85ee57
child 73577 00e0f7724c06
child 73578 0fb889c361e6
NEWS
NEWS
src/HOL/Library/List_Permutation.thy
--- 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)