| changeset 15236 | f289e8ba2bb3 |
| parent 15176 | 2fd60846f485 |
| child 15245 | 5a21d9a8f14b |
--- a/src/HOL/List.thy Mon Oct 11 07:39:19 2004 +0200 +++ b/src/HOL/List.thy Mon Oct 11 07:42:22 2004 +0200 @@ -1007,7 +1007,7 @@ lemma take_take [simp]: "!!xs n. take n (take m xs) = take (min n m) xs" apply (induct m, auto) apply (case_tac xs, auto) -apply (case_tac na, auto) +apply (case_tac n, auto) done lemma drop_drop [simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs"