new lemma splice_length

--- a/src/HOL/List.thy	Wed Apr 25 15:38:56 2007 +0200
+++ b/src/HOL/List.thy	Wed Apr 25 17:50:48 2007 +0200
@@ -2200,6 +2200,12 @@
 
 declare splice.simps(2) [simp del, code del]
 
+lemma length_splice[simp]: "!!ys. length(splice xs ys) = length xs + length ys"
+apply(induct xs) apply simp
+apply(case_tac ys)
+ apply auto
+done
+
 subsubsection{*Sets of Lists*}
 
 subsubsection {* @{text lists}: the list-forming operator over sets *}