NEWS
changeset 57825 58f46c678352
parent 57822 9ea92df3631a
child 57826 a01caa7145d4
     1.1 --- a/NEWS	Mon Jul 28 12:31:30 2014 +0200
     1.2 +++ b/NEWS	Tue Jul 29 17:13:25 2014 +0200
     1.3 @@ -859,6 +859,13 @@
     1.4      bounded_linear_imp_linear ~>  bounded_linear.linear
     1.5  
     1.6  * HOL-Probability:
     1.7 +  - Renamed positive_integral to nn_integral:
     1.8 +
     1.9 +    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
    1.10 +      positive_integral_positive ~> nn_integral_nonneg
    1.11 +
    1.12 +    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
    1.13 +
    1.14    - replaced the Lebesgue integral on real numbers by the more general
    1.15      Bochner integral for functions into a real-normed vector space.
    1.16  
    1.17 @@ -873,14 +880,14 @@
    1.18      integrable_nonneg           ~>  integrableI_nonneg
    1.19      integral_positive           ~>  integral_nonneg_AE
    1.20      integrable_abs_iff          ~>  integrable_abs_cancel
    1.21 -    positive_integral_lim_INF   ~>  positive_integral_liminf
    1.22 +    positive_integral_lim_INF   ~>  nn_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 +    positive_integral_fst       ~>  nn_integral_fst'
    1.31 +    positive_integral_fst_measurable ~> nn_integral_fst
    1.32 +    positive_integral_snd_measurable ~> nn_integral_snd
    1.33  
    1.34      integrable_fst_measurable   ~>
    1.35           integral_fst / integrable_fst / AE_integrable_fst
    1.36 @@ -906,7 +913,7 @@
    1.37           integrable_has_integral_lebesgue_nonneg
    1.38  
    1.39      lebesgue_integral_real_affine  ~>
    1.40 -         positive_integral_real_affine
    1.41 +         nn_integral_real_affine
    1.42  
    1.43      has_integral_iff_positive_integral_lborel  ~>
    1.44           integral_has_integral_nonneg / integrable_has_integral_nonneg
    1.45 @@ -921,13 +928,6 @@
    1.46      integral_cmul_indicator
    1.47      integral_real
    1.48  
    1.49 -  - Renamed positive_integral to nn_integral:
    1.50 -
    1.51 -    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
    1.52 -      positive_integral_positive ~> nn_integral_nonneg
    1.53 -
    1.54 -    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
    1.55 -
    1.56    - Formalized properties about exponentially, Erlang, and normal
    1.57      distributed random variables.
    1.58