# HG changeset patch
# User haftmann
# Date 1749717482 -7200
# Node ID 39a17ff4dd762fdc8e4e5c9ea75438dd057d7d77
# Parent  81f64077eaabfcbed85bc3265523bd85c9678dd2
eliminated transitional lemma

diff -r 81f64077eaab -r 39a17ff4dd76 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 12 10:37:57 2025 +0200
+++ b/src/HOL/List.thy	Thu Jun 12 10:38:02 2025 +0200
@@ -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)