equal
deleted
inserted
replaced
537 by (rotate_tac 3 1); |
537 by (rotate_tac 3 1); |
538 by (dres_inst_tac [("x","e/2")] spec 1 THEN Auto_tac); |
538 by (dres_inst_tac [("x","e/2")] spec 1 THEN Auto_tac); |
539 by (dtac spec 1 THEN Auto_tac); |
539 by (dtac spec 1 THEN Auto_tac); |
540 by (REPEAT(dtac spec 1) THEN Auto_tac); |
540 by (REPEAT(dtac spec 1) THEN Auto_tac); |
541 by (dres_inst_tac [("e","ea/(b - a)")] lemma_straddle 1); |
541 by (dres_inst_tac [("e","ea/(b - a)")] lemma_straddle 1); |
542 by (auto_tac (claset(),simpset() addsimps [real_0_less_divide_iff])); |
542 by (auto_tac (claset(),simpset() addsimps [thm"Ring_and_Field.zero_less_divide_iff"])); |
543 by (rtac exI 1); |
543 by (rtac exI 1); |
544 by (auto_tac (claset(),simpset() addsimps [tpart_def,rsum_def])); |
544 by (auto_tac (claset(),simpset() addsimps [tpart_def,rsum_def])); |
545 by (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = \ |
545 by (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = \ |
546 \ f b - f a" 1); |
546 \ f b - f a" 1); |
547 by (cut_inst_tac [("D","%n. f(D n)"),("m","psize D")] |
547 by (cut_inst_tac [("D","%n. f(D n)"),("m","psize D")] |