| changeset 73443 | 8948519e0a78 |
| parent 73442 | 855a3c18b9c8 |
| child 73510 | c526eb2c7ca0 |
--- 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)