src/HOL/List.ML
changeset 5983 79e301a6a51b
parent 5758 27a2b36efd95
child 6055 fdf4638bf726
     1.1 --- a/src/HOL/List.ML	Fri Nov 27 16:54:59 1998 +0100
     1.2 +++ b/src/HOL/List.ML	Fri Nov 27 17:00:30 1998 +0100
     1.3 @@ -878,12 +878,11 @@
     1.4  Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
     1.5  by(induct_tac "j" 1);
     1.6  by Auto_tac;
     1.7 -by(REPEAT(trans_tac 1));
     1.8  qed "upt_rec";
     1.9  
    1.10  Goal "j<=i ==> [i..j(] = []";
    1.11  by(stac upt_rec 1);
    1.12 -by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
    1.13 +by(Asm_simp_tac 1);
    1.14  qed "upt_conv_Nil";
    1.15  Addsimps [upt_conv_Nil];
    1.16  
    1.17 @@ -901,29 +900,28 @@
    1.18  Goal "length [i..j(] = j-i";
    1.19  by(induct_tac "j" 1);
    1.20   by (Simp_tac 1);
    1.21 -by(asm_simp_tac (simpset() addsimps [Suc_diff_le] addSolver cut_trans_tac) 1);
    1.22 +by(asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
    1.23  qed "length_upt";
    1.24  Addsimps [length_upt];
    1.25  
    1.26  Goal "i+k < j --> [i..j(] ! k = i+k";
    1.27  by(induct_tac "j" 1);
    1.28   by(Simp_tac 1);
    1.29 -by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac
    1.30 -                           addSolver cut_trans_tac) 1);
    1.31 +by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
    1.32  br conjI 1;
    1.33   by(Clarify_tac 1);
    1.34   bd add_lessD1 1;
    1.35 - by(trans_tac 1);
    1.36 + by(Simp_tac 1);
    1.37  by(Clarify_tac 1);
    1.38  br conjI 1;
    1.39   by(Clarify_tac 1);
    1.40   by(subgoal_tac "n=i+k" 1);
    1.41    by(Asm_full_simp_tac 1);
    1.42 - by(trans_tac 1);
    1.43 + by(Simp_tac 1);
    1.44  by(Clarify_tac 1);
    1.45  by(subgoal_tac "n=i+k" 1);
    1.46   by(Asm_full_simp_tac 1);
    1.47 -by(trans_tac 1);
    1.48 +by(Simp_tac 1);
    1.49  qed_spec_mp "nth_upt";
    1.50  Addsimps [nth_upt];
    1.51