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