src/HOL/List.ML
changeset 6073 fba734ba6894
parent 6058 a9600c47ace3
child 6141 a6922171b396
     1.1 --- a/src/HOL/List.ML	Fri Jan 08 14:02:04 1999 +0100
     1.2 +++ b/src/HOL/List.ML	Sat Jan 09 15:24:11 1999 +0100
     1.3 @@ -906,20 +906,10 @@
     1.4  by(induct_tac "j" 1);
     1.5   by(Simp_tac 1);
     1.6  by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
     1.7 -br conjI 1;
     1.8 - by(Clarify_tac 1);
     1.9 - bd add_lessD1 1;
    1.10 - by(Simp_tac 1);
    1.11 -by(Clarify_tac 1);
    1.12 -br conjI 1;
    1.13 - by(Clarify_tac 1);
    1.14 - by(subgoal_tac "n=i+k" 1);
    1.15 -  by(Asm_full_simp_tac 1);
    1.16 - by(Simp_tac 1);
    1.17  by(Clarify_tac 1);
    1.18  by(subgoal_tac "n=i+k" 1);
    1.19 - by(Asm_full_simp_tac 1);
    1.20 -by(Simp_tac 1);
    1.21 + by(Asm_simp_tac 2);
    1.22 +by(Asm_simp_tac 1);
    1.23  qed_spec_mp "nth_upt";
    1.24  Addsimps [nth_upt];
    1.25