equal
deleted
inserted
replaced
1000 \ poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* \ |
1000 \ poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* \ |
1001 \ (qa +++ -- (pderiv q)))))" 1); |
1001 \ (qa +++ -- (pderiv q)))))" 1); |
1002 by (dtac (poly_mult_left_cancel RS iffD1) 1); |
1002 by (dtac (poly_mult_left_cancel RS iffD1) 1); |
1003 by (Asm_full_simp_tac 1); |
1003 by (Asm_full_simp_tac 1); |
1004 by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult, |
1004 by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult, |
1005 poly_minus] delsimps [pmult_Cons, thm"mult_cancel_left"]) 1); |
1005 poly_minus] delsimps [pmult_Cons, mult_cancel_left, field_mult_cancel_left]) 1); |
1006 by (Step_tac 1); |
1006 by (Step_tac 1); |
1007 by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel |
1007 by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel |
1008 RS iffD1) 1); |
1008 RS iffD1) 1); |
1009 by (Simp_tac 1); |
1009 by (Simp_tac 1); |
1010 by (rtac ((CLAIM_SIMP |
1010 by (rtac ((CLAIM_SIMP |