removed assumption from lemma List.take_add
authornoschinl
Mon, 09 May 2011 12:26:25 +0200
changeset 42713 276c8cbeb5d2
parent 42712 574613b47583
child 42714 fcba668b0839
removed assumption from lemma List.take_add
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