# HG changeset patch
# User nipkow
# Date 1615880541 -3600
# Node ID 8948519e0a7867c58dc808c7f5338b25fd18171b
# Parent  855a3c18b9c8b2fdf61bd0f50e2022a370b7a427
tuned lemma

diff -r 855a3c18b9c8 -r 8948519e0a78 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 15 22:58:20 2021 +0100
+++ b/src/HOL/List.thy	Tue Mar 16 08:42:21 2021 +0100
@@ -4372,7 +4372,7 @@
 by (induct xs) simp_all
 
 lemma remove1_split:
-  "a \<in> set xs \<Longrightarrow> \<exists>ls rs. xs = ls @ a # rs \<and> remove1 a xs = ls @ rs"
+  "a \<in> set xs \<Longrightarrow> remove1 a xs = ys \<longleftrightarrow> (\<exists>ls rs. xs = ls @ a # rs \<and> a \<notin> set ls \<and> ys = ls @ rs)"
 by (metis remove1.simps(2) remove1_append split_list_first)