src/HOL/List.ML
changeset 8741 61bc5ed22b62
parent 8442 96023903c2df
child 8935 548901d05a0e
     1.1 --- a/src/HOL/List.ML	Tue Apr 18 15:56:41 2000 +0200
     1.2 +++ b/src/HOL/List.ML	Wed Apr 19 11:09:59 2000 +0200
     1.3 @@ -560,6 +560,7 @@
     1.4  Goal "length (filter P xs) <= length xs";
     1.5  by (induct_tac "xs" 1);
     1.6  by Auto_tac;
     1.7 +by (asm_simp_tac (simpset() addsimps [le_SucI]) 1);
     1.8  qed "length_filter";
     1.9  Addsimps[length_filter];
    1.10