--- 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.
--- 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