merged
authorwenzelm
Thu, 12 Jun 2025 16:54:28 +0200
changeset 82698 c0f166b39a3a
parent 82694 39a17ff4dd76 (diff)
parent 82697 cc05bc2cfb2f (current diff)
child 82699 a3e7732b0393
child 82700 2e139be2d136
merged
--- 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)