equal
deleted
inserted
replaced
478 apply (unfold fderiv_def) |
478 apply (unfold fderiv_def) |
479 apply (simp add: bounded_bilinear_mult.bounded_linear_left) |
479 apply (simp add: bounded_bilinear_mult.bounded_linear_left) |
480 apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) |
480 apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric]) |
481 apply (subst diff_divide_distrib) |
481 apply (subst diff_divide_distrib) |
482 apply (subst times_divide_eq_left [symmetric]) |
482 apply (subst times_divide_eq_left [symmetric]) |
483 apply (simp cong: LIM_cong add: divide_self) |
483 apply (simp cong: LIM_cong) |
484 apply (simp add: LIM_norm_zero_iff LIM_zero_iff) |
484 apply (simp add: LIM_norm_zero_iff LIM_zero_iff) |
485 done |
485 done |
486 |
486 |
487 end |
487 end |