# HG changeset patch # User nipkow # Date 1144604490 -7200 # Node ID 6c7383f80ad195c08133076599c0f7760fa971b2 # Parent 0d57259fea8288ca476e17a49a72b2f1a1ff30e5 Added function "splice" diff -r 0d57259fea82 -r 6c7383f80ad1 src/HOL/List.thy --- a/src/HOL/List.thy Sun Apr 09 19:29:44 2006 +0200 +++ b/src/HOL/List.thy Sun Apr 09 19:41:30 2006 +0200 @@ -44,6 +44,7 @@ replicate :: "nat => 'a => 'a list" rotate1 :: "'a list \ 'a list" rotate :: "nat \ 'a list \ 'a list" + splice :: "'a list \ 'a list \ 'a list" sublist :: "'a list => nat set => 'a list" (* For efficiency *) mem :: "'a => 'a list => bool" (infixl 55) @@ -214,6 +215,11 @@ "sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..