src/HOL/List.ML
changeset 6058 a9600c47ace3
parent 6055 fdf4638bf726
child 6073 fba734ba6894
     1.1 --- a/src/HOL/List.ML	Mon Jan 04 16:13:57 1999 +0100
     1.2 +++ b/src/HOL/List.ML	Mon Jan 04 16:37:04 1999 +0100
     1.3 @@ -856,8 +856,7 @@
     1.4  *)
     1.5  Goal "!n::nat. m <= n --> m <= foldl op+ n ns";
     1.6  by (induct_tac "ns" 1);
     1.7 - by (Simp_tac 1);
     1.8 -by (Asm_full_simp_tac 1);
     1.9 +by Auto_tac;
    1.10  qed_spec_mp "start_le_sum";
    1.11  
    1.12  Goal "n : set ns ==> n <= foldl op+ 0 ns";