diff -r d8986d88295e -r 3b98b1b57435 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jun 16 12:19:23 2025 +0200
+++ b/src/HOL/List.thy	Mon Jun 16 15:25:38 2025 +0200
@@ -7988,19 +7988,28 @@
   and \<^const>\<open>list_ex1\<close> in specifications.
 \<close>
 
-lemma list_all_simps [code]:
-  \<open>list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs\<close>
+lemma list_all_Nil_iff [code, no_atp]:
   \<open>list_all P [] \<longleftrightarrow> True\<close>
-  by (simp_all add: list_all_iff)
-
-lemma list_ex_simps [simp, code]:
+  by (simp add: list_all_iff)
+
+lemma list_all_Cons_iff [code, no_atp]:
+  \<open>list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs\<close>
+  by (simp add: list_all_iff)
+
+lemma list_ex_Nil_iff [simp, code, no_atp]:
+  \<open>list_ex P [] \<longleftrightarrow> False\<close>
+  by (simp add: list_ex_iff)
+
+lemma list_ex_Cons_iff [simp, code, no_atp]:
   \<open>list_ex P (x # xs) \<longleftrightarrow> P x \<or> list_ex P xs\<close>
-  \<open>list_ex P [] \<longleftrightarrow> False\<close>
-  by (simp_all add: list_ex_iff)
-
-lemma list_ex1_simps [simp, code]:
-  \<open>list_ex1 P [] = False\<close>
-  \<open>list_ex1 P (x # xs) = (if P x then list_all (\<lambda>y. \<not> P y \<or> x = y) xs else list_ex1 P xs)\<close>
+  by (simp add: list_ex_iff)
+
+lemma list_ex1_Nil_iff [simp, code, no_atp]:
+  \<open>list_ex1 P [] \<longleftrightarrow> False\<close>
+  by (auto simp add: list_ex1_iff)
+
+lemma list_ex1_Cons_iff [simp, code, no_atp]:
+  \<open>list_ex1 P (x # xs) \<longleftrightarrow> (if P x then list_all (\<lambda>y. \<not> P y \<or> x = y) xs else list_ex1 P xs)\<close>
   by (auto simp add: list_ex1_iff list_all_iff)
 
 lemma list_all_append [simp]: