src/HOL/List.ML
changeset 6055 fdf4638bf726
parent 5983 79e301a6a51b
child 6058 a9600c47ace3
     1.1 --- a/src/HOL/List.ML	Mon Dec 28 17:03:47 1998 +0100
     1.2 +++ b/src/HOL/List.ML	Mon Jan 04 15:07:47 1999 +0100
     1.3 @@ -858,7 +858,6 @@
     1.4  by (induct_tac "ns" 1);
     1.5   by (Simp_tac 1);
     1.6  by (Asm_full_simp_tac 1);
     1.7 -by (blast_tac (claset() addIs [trans_le_add1]) 1);
     1.8  qed_spec_mp "start_le_sum";
     1.9  
    1.10  Goal "n : set ns ==> n <= foldl op+ 0 ns";