Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
eliminated transitional lemma
authorhaftmann
Thu, 12 Jun 2025 10:38:02 +0200
changeset 82694 39a17ff4dd76
parent 82693 81f64077eaab
child 82698 c0f166b39a3a
eliminated transitional lemma
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle