author | nipkow |
Fri, 01 Aug 1997 10:59:19 +0200 (1997-08-01) | |
changeset 3585 | 5b2dcdc1829c |
parent 3584 | 8f9ee0f79d9a |
child 3586 | 2ee1ed79c802 |
src/HOL/List.ML | file | annotate | diff | comparison | revisions |
--- 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);