src/HOL/UNITY/AllocBase.ML
changeset 9109 0085c32a533b
parent 9107 67202a50ee6d
child 9336 9ae89b9ce206
     1.1 --- a/src/HOL/UNITY/AllocBase.ML	Thu Jun 22 23:04:34 2000 +0200
     1.2 +++ b/src/HOL/UNITY/AllocBase.ML	Fri Jun 23 10:33:11 2000 +0200
     1.3 @@ -9,13 +9,14 @@
     1.4  time_use_thy "AllocBase";
     1.5  *)
     1.6  
     1.7 -Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n";
     1.8 +Goal "!!f :: nat=>nat. \
     1.9 +\     (ALL i. i<n --> f i <= g i) --> \
    1.10 +\     setsum f (lessThan n) <= setsum g (lessThan n)";
    1.11  by (induct_tac "n" 1);
    1.12 -by Auto_tac;
    1.13 +by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
    1.14  by (dres_inst_tac [("x","n")] spec 1);
    1.15 -by Auto_tac;
    1.16  by (arith_tac 1);
    1.17 -qed_spec_mp "sum_mono";
    1.18 +qed_spec_mp "setsum_fun_mono";
    1.19  
    1.20  Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
    1.21  by (induct_tac "ys" 1);