src/HOL/List.ML
changeset 5758 27a2b36efd95
parent 5644 85fd64148873
child 5983 79e301a6a51b
     1.1 --- a/src/HOL/List.ML	Fri Oct 23 20:36:21 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Fri Oct 23 20:44:34 1998 +0200
     1.3 @@ -862,8 +862,8 @@
     1.4  qed_spec_mp "start_le_sum";
     1.5  
     1.6  Goal "n : set ns ==> n <= foldl op+ 0 ns";
     1.7 -by (auto_tac (claset() addIs [start_le_sum],
     1.8 -             simpset() addsimps [in_set_conv_decomp]));
     1.9 +by (force_tac (claset() addIs [start_le_sum],
    1.10 +              simpset() addsimps [in_set_conv_decomp]) 1);
    1.11  qed "elem_le_sum";
    1.12  
    1.13  Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";