NEWS
authorhoelzl
Wed Mar 19 15:35:07 2014 +0100 (2014-03-19)
changeset 56214d503c51e869a
parent 56213 e5720d3c18f0
child 56216 76ff0a15d202
NEWS
NEWS
     1.1 --- a/NEWS	Wed Mar 19 15:34:57 2014 +0100
     1.2 +++ b/NEWS	Wed Mar 19 15:35:07 2014 +0100
     1.3 @@ -412,6 +412,53 @@
     1.4  shows up as additional case in fixpoint induction proofs.
     1.5  INCOMPATIBILITY
     1.6  
     1.7 +* Removed and renamed theorems in Series:
     1.8 +  summable_le         ~>  suminf_le
     1.9 +  suminf_le           ~>  suminf_le_const
    1.10 +  series_pos_le       ~>  setsum_le_suminf
    1.11 +  series_pos_less     ~>  setsum_less_suminf
    1.12 +  suminf_ge_zero      ~>  suminf_nonneg
    1.13 +  suminf_gt_zero      ~>  suminf_pos
    1.14 +  suminf_gt_zero_iff  ~>  suminf_pos_iff
    1.15 +  summable_sumr_LIMSEQ_suminf  ~>  summable_LIMSEQ
    1.16 +  suminf_0_le         ~>  suminf_nonneg [rotate]
    1.17 +  pos_summable        ~>  summableI_nonneg_bounded
    1.18 +  ratio_test          ~>  summable_ratio_test
    1.19 +
    1.20 +  removed series_zero, replaced by sums_finite
    1.21 +
    1.22 +  removed auxiliary lemmas:
    1.23 +    sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
    1.24 +    half, le_Suc_ex_iff, lemma_realpow_diff_sumr, real_setsum_nat_ivl_bounded,
    1.25 +    summable_le2, ratio_test_lemma2, sumr_minus_one_realpow_zerom,
    1.26 +    sumr_one_lb_realpow_zero, summable_convergent_sumr_iff, sumr_diff_mult_const
    1.27 +INCOMPATIBILITY.
    1.28 +
    1.29 +* Replace (F)DERIV syntax by has_derivative:
    1.30 +  - "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'"
    1.31 +
    1.32 +  - "(f has_field_derivative f') (at x within s)" replaces "DERIV f x : s : f'"
    1.33 +
    1.34 +  - "f differentiable at x within s" replaces "_ differentiable _ in _" syntax
    1.35 +
    1.36 +  - removed constant isDiff
    1.37 +
    1.38 +  - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as input
    1.39 +    syntax.
    1.40 +
    1.41 +  - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed
    1.42 +
    1.43 +  - Renamed FDERIV_... lemmas to has_derivative_...
    1.44 +
    1.45 +  - Other renamings:
    1.46 +    differentiable_def        ~>  real_differentiable_def
    1.47 +    differentiableE           ~>  real_differentiableE
    1.48 +    fderiv_def                ~>  has_derivative_at
    1.49 +    field_fderiv_def          ~>  field_has_derivative_at
    1.50 +    isDiff_der                ~>  differentiable_def
    1.51 +    deriv_fderiv              ~>  has_field_derivative_def
    1.52 +INCOMPATIBILITY.
    1.53 +
    1.54  * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
    1.55  
    1.56  * Nitpick: