equal
deleted
inserted
replaced
1313 |
1313 |
1314 (*Can't get rid of x \\<noteq> 0 because it isn't continuous at zero*) |
1314 (*Can't get rid of x \\<noteq> 0 because it isn't continuous at zero*) |
1315 Goalw [nsderiv_def] |
1315 Goalw [nsderiv_def] |
1316 "x \\<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"; |
1316 "x \\<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))"; |
1317 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1); |
1317 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1); |
1318 by (forward_tac [Infinitesimal_add_not_zero] 1); |
1318 by (ftac Infinitesimal_add_not_zero 1); |
1319 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2); |
1319 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2); |
1320 by (auto_tac (claset(), |
1320 by (auto_tac (claset(), |
1321 simpset() addsimps [starfun_inverse_inverse, realpow_two] |
1321 simpset() addsimps [starfun_inverse_inverse, realpow_two] |
1322 delsimps [hypreal_minus_mult_eq1 RS sym, |
1322 delsimps [hypreal_minus_mult_eq1 RS sym, |
1323 hypreal_minus_mult_eq2 RS sym])); |
1323 hypreal_minus_mult_eq2 RS sym])); |