# HG changeset patch
# User noschinl
# Date 1304936785 -7200
# Node ID 276c8cbeb5d22f70d9a710613660ef8b829a4fb1
# Parent  574613b47583cdf7ff119433cabd47a3db60bc2b
removed assumption from lemma List.take_add

diff -r 574613b47583 -r 276c8cbeb5d2 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 06 20:25:41 2011 +0200
+++ b/src/HOL/List.thy	Mon May 09 12:26:25 2011 +0200
@@ -1814,7 +1814,7 @@
 done
 
 lemma take_add: 
-  "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
+  "take (i+j) xs = take i xs @ take j (drop i xs)"
 apply (induct xs arbitrary: i, auto) 
 apply (case_tac i, simp_all)
 done