--- a/src/HOL/List.thy Tue Oct 09 13:06:39 2018 +0200
+++ b/src/HOL/List.thy Thu Oct 11 15:35:18 2018 +0200
@@ -4534,6 +4534,10 @@
lemma split_Nil_iff[simp]: "splice xs ys = [] \<longleftrightarrow> xs = [] \<and> ys = []"
by (induct xs ys rule: splice.induct) auto
+lemma splice_replicate[simp]: "splice (replicate m x) (replicate n x) = replicate (m+n) x"
+apply(induction "replicate m x" "replicate n x" arbitrary: m n rule: splice.induct)
+apply (auto simp add: Cons_replicate_eq dest: gr0_implies_Suc)
+done
subsubsection \<open>@{const shuffles}\<close>