NEWS
changeset 56993 e5366291d6aa
parent 56964 5bee93b2020d
child 56996 891e992e510f
     1.1 --- a/NEWS	Mon May 19 11:27:02 2014 +0200
     1.2 +++ b/NEWS	Mon May 19 12:04:45 2014 +0200
     1.3 @@ -670,6 +670,68 @@
     1.4      derivative_is_linear      ~>  has_derivative_linear
     1.5      bounded_linear_imp_linear ~>  bounded_linear.linear
     1.6  
     1.7 +* HOL-Probability:
     1.8 +  - replaced the Lebesgue integral on real numbers by the more general Bochner
     1.9 +    integral for functions into a real-normed vector space.
    1.10 +
    1.11 +    integral_zero               ~>  integral_zero / integrable_zero
    1.12 +    integral_minus              ~>  integral_minus / integrable_minus
    1.13 +    integral_add                ~>  integral_add / integrable_add
    1.14 +    integral_diff               ~>  integral_diff / integrable_diff
    1.15 +    integral_setsum             ~>  integral_setsum / integrable_setsum
    1.16 +    integral_multc              ~>  integral_mult_left / integrable_mult_left
    1.17 +    integral_cmult              ~>  integral_mult_right / integrable_mult_right
    1.18 +    integral_triangle_inequality~>  integral_norm_bound
    1.19 +    integrable_nonneg           ~>  integrableI_nonneg
    1.20 +    integral_positive           ~>  integral_nonneg_AE
    1.21 +    integrable_abs_iff          ~>  integrable_abs_cancel
    1.22 +    positive_integral_lim_INF   ~>  positive_integral_liminf
    1.23 +    lebesgue_real_affine        ~>  lborel_real_affine
    1.24 +    borel_integral_has_integral ~>  has_integral_lebesgue_integral
    1.25 +    integral_indicator          ~>
    1.26 +         integral_real_indicator / integrable_real_indicator
    1.27 +    positive_integral_fst       ~>  positive_integral_fst'
    1.28 +    positive_integral_fst_measurable ~> positive_integral_fst
    1.29 +    positive_integral_snd_measurable ~> positive_integral_snd
    1.30 +
    1.31 +    integrable_fst_measurable   ~>
    1.32 +         integral_fst / integrable_fst / AE_integrable_fst
    1.33 +
    1.34 +    integrable_snd_measurable   ~>
    1.35 +         integral_snd / integrable_snd / AE_integrable_snd
    1.36 +
    1.37 +    integral_monotone_convergence  ~>
    1.38 +         integral_monotone_convergence / integrable_monotone_convergence
    1.39 +
    1.40 +    integral_monotone_convergence_at_top  ~>
    1.41 +         integral_monotone_convergence_at_top /
    1.42 +         integrable_monotone_convergence_at_top
    1.43 +
    1.44 +    has_integral_iff_positive_integral_lebesgue  ~>
    1.45 +         has_integral_iff_has_bochner_integral_lebesgue_nonneg
    1.46 +
    1.47 +    lebesgue_integral_has_integral  ~>
    1.48 +         has_integral_integrable_lebesgue_nonneg
    1.49 +
    1.50 +    positive_integral_lebesgue_has_integral  ~>
    1.51 +         integral_has_integral_lebesgue_nonneg /
    1.52 +         integrable_has_integral_lebesgue_nonneg
    1.53 +
    1.54 +    lebesgue_integral_real_affine  ~>
    1.55 +         positive_integral_real_affine
    1.56 +
    1.57 +    has_integral_iff_positive_integral_lborel  ~>
    1.58 +         integral_has_integral_nonneg / integrable_has_integral_nonneg
    1.59 +
    1.60 +    The following theorems where removed:
    1.61 +
    1.62 +    lebesgue_integral_nonneg
    1.63 +    lebesgue_integral_uminus
    1.64 +    lebesgue_integral_cmult
    1.65 +    lebesgue_integral_multc
    1.66 +    lebesgue_integral_cmult_nonneg
    1.67 +    integral_cmul_indicator
    1.68 +    integral_real
    1.69  
    1.70  *** Scala ***
    1.71