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.
tuned lemma
authornipkow
Tue, 16 Mar 2021 08:42:21 +0100
changeset 73443 8948519e0a78
parent 73442 855a3c18b9c8
child 73444 02ea468ecf07
tuned lemma
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle