| changeset 3292 | 8b143c196d42 |
| parent 3283 | 0db086394024 |
| child 3342 | ec3b55fcb165 |
--- a/src/HOL/List.ML Thu May 22 12:59:08 1997 +0200 +++ b/src/HOL/List.ML Thu May 22 13:05:52 1997 +0200 @@ -464,7 +464,7 @@ by(exhaust_tac "n" 1); by(Blast_tac 1); by(exhaust_tac "i" 1); -by(ALLGOALS (hyp_subst_tac THEN' Asm_full_simp_tac)); +by(ALLGOALS Asm_full_simp_tac); qed_spec_mp "nth_take"; Addsimps [nth_take];