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