# HG changeset patch
# User nipkow
# Date 1699476302 -3600
# Node ID ab85d87dc2beb7649640d72b92be24a9bc606918
# Parent  2fee5fba3116771dc0930e4e1f89e9e57369f3ed# Parent  9e43ab263d338f586dbf968e11a1b9cf6f7162de
merged

diff -r 2fee5fba3116 -r ab85d87dc2be src/HOL/Library/NList.thy
--- a/src/HOL/Library/NList.thy	Wed Nov 08 20:31:29 2023 +0100
+++ b/src/HOL/Library/NList.thy	Wed Nov 08 21:45:02 2023 +0100
@@ -20,6 +20,9 @@
 lemma nlistsE_length [simp]: "xs \<in> nlists n A \<Longrightarrow> size xs = n"
   by (simp add: nlists_def)
 
+lemma in_nlists_UNIV: "xs \<in> nlists k UNIV \<longleftrightarrow> length xs = k"
+unfolding nlists_def by(auto)
+
 lemma less_lengthI: "\<lbrakk> xs \<in> nlists n A; p < n \<rbrakk> \<Longrightarrow> p < size xs"
 by (simp)