| changeset 4681 | a331c1f5a23e |
| parent 4647 | 42af8ae6e2c1 |
| child 4686 | 74a12e86b20b |
--- a/src/HOL/List.ML Thu Mar 05 10:47:27 1998 +0100 +++ b/src/HOL/List.ML Fri Mar 06 15:19:29 1998 +0100 @@ -479,9 +479,6 @@ by (rtac allI 1); by (exhaust_tac "xs" 1); by (ALLGOALS Asm_simp_tac); -by (rtac allI 1); -by (exhaust_tac "xs" 1); - by (ALLGOALS Asm_simp_tac); qed_spec_mp "nth_append"; goal thy "!n. n < length xs --> (map f xs)!n = f(xs!n)";