--- 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>