# HG changeset patch
# User nipkow
# Date 1539027111 -7200
# Node ID d4baf535f84577b9ff81d74f5f623e279cc8f0bd
# Parent  be20f5f6feb9d705f8d5528cb86924dc9ff24418
added simp-lemma

diff -r be20f5f6feb9 -r d4baf535f845 src/HOL/List.thy
--- 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>