# HG changeset patch
# User nipkow
# Date 1660211839 -7200
# Node ID dd04e81172a8b38cb41ea1dead1a31ff76f01dab
# Parent  40e16228405e1ff4cd7b76ce2720d8f814856354
nlists is picked up automatically but conflicts with the RBT setup

diff -r 40e16228405e -r dd04e81172a8 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Thu Aug 11 10:11:21 2022 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Thu Aug 11 11:57:19 2022 +0200
@@ -29,6 +29,7 @@
   Euclidean_Algorithm.Lcm
   "Gcd :: _ poly set \<Rightarrow> _"
   "Lcm :: _ poly set \<Rightarrow> _"
+  nlists
 ]]
 
 text \<open>
diff -r 40e16228405e -r dd04e81172a8 src/HOL/Library/NList.thy
--- a/src/HOL/Library/NList.thy	Thu Aug 11 10:11:21 2022 +0200
+++ b/src/HOL/Library/NList.thy	Thu Aug 11 11:57:19 2022 +0200
@@ -14,11 +14,11 @@
 lemma nlistsI: "\<lbrakk> size xs = n; set xs \<subseteq> A \<rbrakk> \<Longrightarrow> xs \<in> nlists n A"
   by (simp add: nlists_def)
 
-lemma nlistsE_length [simp](*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> size xs = n"
+lemma nlistsE_length (*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> size xs = n"
   by (simp add: nlists_def)
 
 lemma less_lengthI: "\<lbrakk> xs \<in> nlists n A; p < n \<rbrakk> \<Longrightarrow> p < size xs"
-by (simp)
+by (simp add: nlistsE_length)
 
 lemma nlistsE_set[simp](*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> set xs \<subseteq> A"
 unfolding nlists_def by (simp)
@@ -27,7 +27,7 @@
 assumes "A \<subseteq> B" shows "nlists n A \<subseteq> nlists n B"
 proof
   fix xs assume "xs \<in> nlists n A"
-  then obtain size: "size xs = n" and inA: "set xs \<subseteq> A" by simp
+  then obtain size: "size xs = n" and inA: "set xs \<subseteq> A" by (simp add:nlistsE_length)
   with assms have "set xs \<subseteq> B" by simp
   with size show "xs \<in> nlists n B" by(clarsimp intro!: nlistsI)
 qed