# HG changeset patch
# User nipkow
# Date 1085416534 -7200
# Node ID e05116289ff9f3250bd0b97f7916de795ba3a85c
# Parent  2d27b5ebc4471d0258ee267aa9f5699769b196ba
added drop_take:thm

diff -r 2d27b5ebc447 -r e05116289ff9 src/HOL/List.thy
--- 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)