# HG changeset patch
# User nipkow
# Date 1660205481 -7200
# Node ID 40e16228405e1ff4cd7b76ce2720d8f814856354
# Parent  2a049b402e535c8048bc945675b59c054a84d882
new lemma

diff -r 2a049b402e53 -r 40e16228405e NEWS
--- a/NEWS	Thu Aug 11 05:50:48 2022 +0200
+++ b/NEWS	Thu Aug 11 10:11:21 2022 +0200
@@ -41,6 +41,8 @@
 integers, sacrificing pattern patching in exchange for dramatically
 increased performance for comparisions.
 
+* New theory HOL-Library.NList of fixed length lists
+
 * Rule split_of_bool_asm is not split any longer, analogously to
 split_if_asm.  INCOMPATIBILITY.
 
diff -r 2a049b402e53 -r 40e16228405e src/HOL/Library/NList.thy
--- a/src/HOL/Library/NList.thy	Thu Aug 11 05:50:48 2022 +0200
+++ b/src/HOL/Library/NList.thy	Thu Aug 11 10:11:21 2022 +0200
@@ -95,4 +95,7 @@
 lemma nlists_replicateI [intro]: "x \<in> A \<Longrightarrow> replicate n x \<in> nlists n A"
  by (induct n) auto
 
+lemma nlists_set[code]: "nlists n (set xs) = set (List.n_lists n xs)"
+unfolding nlists_def by (rule sym, induct n) (auto simp: image_iff length_Suc_conv)
+
 end