# HG changeset patch
# User nipkow
# Date 1539264918 -7200
# Node ID f2d233f6356caee252b44b52c46820b0847f134e
# Parent  4f3d93f0ba94adabfc82f1cfb94bce27d9ce2ea6
added simp-lemma

diff -r 4f3d93f0ba94 -r f2d233f6356c src/HOL/List.thy
--- 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>