# HG changeset patch
# User paulson
# Date 1054111674 -7200
# Node ID 826037db30cdbfc7ad344fb85415640b99ad02f0
# Parent  ef1da11a64b9b6f89ed00feb88461aee01ec2bee
new theorem

diff -r ef1da11a64b9 -r 826037db30cd 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} *}