# HG changeset patch
# User haftmann
# Date 1750346140 -7200
# Node ID 89347c0cc6a391a0a8a23d8ffe99d43910966e62
# Parent  8b537e1af2ec93431dab0eec825549b79c791dbd
treat map_filter similar to list_all, list_ex, list_ex1

diff -r 8b537e1af2ec -r 89347c0cc6a3 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jun 17 14:11:40 2025 +0200
+++ b/src/HOL/List.thy	Thu Jun 19 17:15:40 2025 +0200
@@ -8306,9 +8306,9 @@
   intermediate lists on execution -- do not use for proving.
 \<close>
 
-lemma map_filter_simps [code]:
+lemma map_filter_simps [simp, code, no_atp]:
+  \<open>map_filter f [] = []\<close>
   \<open>map_filter f (x # xs) = (case f x of None \<Rightarrow> map_filter f xs | Some y \<Rightarrow> y # map_filter f xs)\<close>
-  \<open>map_filter f [] = []\<close>
   by (simp_all add: map_filter_def split: option.split)
 
 lemma map_filter_map_filter [code_unfold]: