new theorem
authorpaulson
Wed May 28 10:47:54 2003 +0200 (2003-05-28)
changeset 14050826037db30cd
parent 14049 ef1da11a64b9
child 14051 4b61bbb0dcab
new theorem
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Tue May 27 17:39:43 2003 +0200
     1.2 +++ b/src/HOL/List.thy	Wed May 28 10:47:54 2003 +0200
     1.3 @@ -885,6 +885,12 @@
     1.4  apply auto
     1.5  done
     1.6  
     1.7 +lemma take_add [rule_format]: 
     1.8 +    "\<forall>i. i+j \<le> length(xs) --> take (i+j) xs = take i xs @ take j (drop i xs)"
     1.9 +apply (induct xs, auto) 
    1.10 +apply (case_tac i, simp_all) 
    1.11 +done
    1.12 +
    1.13  
    1.14  subsection {* @{text takeWhile} and @{text dropWhile} *}
    1.15