changeset 22793 | dc13dfd588b2 |
parent 22633 | a47e4fd7ebc1 |
child 22799 | ed7d53db2170 |
--- 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 *}