--- a/src/HOL/List.thy Thu Jun 12 12:59:17 2025 +0200
+++ b/src/HOL/List.thy Thu Jun 12 16:54:28 2025 +0200
@@ -7945,7 +7945,7 @@
text \<open>Executable checks for relations on sets\<close>
definition listrel1p :: \<open>('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> \<comment> \<open>only for code generation\<close>
- where \<open>listrel1p r xs ys \<longleftrightarrow> (xs, ys) \<in> listrel1 {(x, y). r x y}\<close>
+ where \<open>listrel1p r xs ys \<longleftrightarrow> (xs, ys) \<in> listrel1 {(x, y). r x y}\<close>
lemma [code_unfold]:
\<open>(xs, ys) \<in> listrel1 r \<longleftrightarrow> listrel1p (\<lambda>x y. (x, y) \<in> r) xs ys\<close>
@@ -8711,10 +8711,6 @@
subsection \<open>Misc\<close>
-lemma map_rec:
- "map f xs = rec_list Nil (%x _ y. Cons (f x) y) xs"
- by (induct xs) auto
-
lemma Ball_set_list_all: (* FIXME delete candidate *)
"Ball (set xs) P \<longleftrightarrow> list_all P xs"
by (fact Ball_set)