# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1539071593 -7200
# Node ID 9e12bbe91471d4a453dd6548cc8cebbd4c505eeb
# Parent  90fce429e1bc8ab914db19685fc4af739ba009c2# Parent  d4baf535f84577b9ff81d74f5f623e279cc8f0bd
merged

diff -r 90fce429e1bc -r 9e12bbe91471 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Oct 08 17:12:28 2018 +0200
+++ b/src/HOL/List.thy	Tue Oct 09 09:53:13 2018 +0200
@@ -4529,7 +4529,10 @@
 by (cases xs) simp_all
 
 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
-  by (induct xs ys rule: splice.induct) auto
+by (induct xs ys rule: splice.induct) auto
+
+lemma split_Nil_iff[simp]: "splice xs ys = [] \<longleftrightarrow> xs = [] \<and> ys = []"
+by (induct xs ys rule: splice.induct) auto
 
 
 subsubsection \<open>@{const shuffles}\<close>