| changeset 3585 | 5b2dcdc1829c |
| parent 3574 | 5995ab73d790 |
| child 3586 | 2ee1ed79c802 |
--- a/src/HOL/List.ML Fri Aug 01 09:42:19 1997 +0200 +++ b/src/HOL/List.ML Fri Aug 01 10:59:19 1997 +0200 @@ -558,7 +558,7 @@ qed_spec_mp "nth_take"; Addsimps [nth_take]; -goal thy "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs"; +goal thy "!xs i. n + i <= length xs --> nth i (drop n xs) = nth (n + i) xs"; by (nat_ind_tac "n" 1); by (ALLGOALS Asm_simp_tac); by (rtac allI 1);