added drop_take:thm

--- a/src/HOL/List.thy	Fri May 21 21:49:45 2004 +0200
+++ b/src/HOL/List.thy	Mon May 24 18:35:34 2004 +0200
@@ -889,6 +889,12 @@
 apply (case_tac xs, auto)
 done
 
+lemma drop_take: "!!m n. drop n (take m xs) = take (m-n) (drop n xs)"
+apply(induct xs)
+ apply simp
+apply(simp add: take_Cons drop_Cons split:nat.split)
+done
+
 lemma append_take_drop_id [simp]: "!!xs. take n xs @ drop n xs = xs"
 apply (induct n, auto)
 apply (case_tac xs, auto)