[isabelle-dev] NEWS: clean up Series and Deriv in Complex_Main

[Johannes Hölzl]

* Removed and renamed theorems in Series:
  summable_le         ~>  suminf_le
  suminf_le           ~>  suminf_le_const
  series_pos_le       ~>  setsum_le_suminf
  series_pos_less     ~>  setsum_less_suminf
  suminf_ge_zero      ~>  suminf_nonneg
  suminf_gt_zero      ~>  suminf_pos
  suminf_gt_zero_iff  ~>  suminf_pos_iff
  summable_sumr_LIMSEQ_suminf  ~>  summable_LIMSEQ
  suminf_0_le         ~>  suminf_nonneg [rotate]
  pos_summable        ~>  summableI_nonneg_bounded
  ratio_test          ~>  summable_ratio_test

  removed series_zero, replaced by sums_finite

  removed auxiliary lemmas:
    sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
    half, le_Suc_ex_iff, lemma_realpow_diff_sumr,
real_setsum_nat_ivl_bounded,
    summable_le2, ratio_test_lemma2, sumr_minus_one_realpow_zerom,
    sumr_one_lb_realpow_zero, summable_convergent_sumr_iff,
sumr_diff_mult_const
INCOMPATIBILITY.

* Replace (F)DERIV syntax by has_derivative:
  - "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s :
f'"

  - "(f has_field_derivative f') (at x within s)" replaces "DERIV f x :
s : f'"

  - "f differentiable at x within s" replaces "_ differentiable _ in _"
syntax

  - removed constant isDiff

  - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as
input
    syntax.

  - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed

  - Renamed FDERIV_... lemmas to has_derivative_...

  - Other renamings:
    differentiable_def        ~>  real_differentiable_def
    differentiableE           ~>  real_differentiableE
    fderiv_def                ~>  has_derivative_at
    field_fderiv_def          ~>  field_has_derivative_at
    isDiff_der                ~>  differentiable_def
    deriv_fderiv              ~>  has_field_derivative_def
INCOMPATIBILITY.