--- a/src/HOL/List.thy Mon Oct 08 15:42:43 2018 +0200
+++ b/src/HOL/List.thy Mon Oct 08 21:31:51 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>