author | noschinl |
Mon, 09 May 2011 12:26:25 +0200 | |
changeset 42713 | 276c8cbeb5d2 |
parent 42712 | 574613b47583 |
child 42714 | fcba668b0839 |
src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- 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