src/HOL/List.thy

--- a/src/HOL/List.thy	Tue May 27 17:39:43 2003 +0200
+++ b/src/HOL/List.thy	Wed May 28 10:47:54 2003 +0200
@@ -885,6 +885,12 @@
 apply auto
 done
 
+lemma take_add [rule_format]: 
+    "\<forall>i. i+j \<le> length(xs) --> take (i+j) xs = take i xs @ take j (drop i xs)"
+apply (induct xs, auto) 
+apply (case_tac i, simp_all) 
+done
+
 
 subsection {* @{text takeWhile} and @{text dropWhile} *}