equal
deleted
inserted
replaced
477 by (nat_ind_tac "n" 1); |
477 by (nat_ind_tac "n" 1); |
478 by (Asm_simp_tac 1); |
478 by (Asm_simp_tac 1); |
479 by (rtac allI 1); |
479 by (rtac allI 1); |
480 by (exhaust_tac "xs" 1); |
480 by (exhaust_tac "xs" 1); |
481 by (ALLGOALS Asm_simp_tac); |
481 by (ALLGOALS Asm_simp_tac); |
482 by (rtac allI 1); |
|
483 by (exhaust_tac "xs" 1); |
|
484 by (ALLGOALS Asm_simp_tac); |
|
485 qed_spec_mp "nth_append"; |
482 qed_spec_mp "nth_append"; |
486 |
483 |
487 goal thy "!n. n < length xs --> (map f xs)!n = f(xs!n)"; |
484 goal thy "!n. n < length xs --> (map f xs)!n = f(xs!n)"; |
488 by (induct_tac "xs" 1); |
485 by (induct_tac "xs" 1); |
489 (* case [] *) |
486 (* case [] *) |