# HG changeset patch
# User hoelzl
# Date 1406646805 -7200
# Node ID 58f46c678352dac8f066d5f1c83726fbe2aa4cbd
# Parent  615223745d4eb0e9fef032fc366aa02f475fa74a
better ordering of positive_integral renaming to nn_integral in NEWS

diff -r 615223745d4e -r 58f46c678352 NEWS
--- a/NEWS	Mon Jul 28 12:31:30 2014 +0200
+++ b/NEWS	Tue Jul 29 17:13:25 2014 +0200
@@ -859,6 +859,13 @@
     bounded_linear_imp_linear ~>  bounded_linear.linear
 
 * HOL-Probability:
+  - Renamed positive_integral to nn_integral:
+
+    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
+      positive_integral_positive ~> nn_integral_nonneg
+
+    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
+
   - replaced the Lebesgue integral on real numbers by the more general
     Bochner integral for functions into a real-normed vector space.
 
@@ -873,14 +880,14 @@
     integrable_nonneg           ~>  integrableI_nonneg
     integral_positive           ~>  integral_nonneg_AE
     integrable_abs_iff          ~>  integrable_abs_cancel
-    positive_integral_lim_INF   ~>  positive_integral_liminf
+    positive_integral_lim_INF   ~>  nn_integral_liminf
     lebesgue_real_affine        ~>  lborel_real_affine
     borel_integral_has_integral ~>  has_integral_lebesgue_integral
     integral_indicator          ~>
          integral_real_indicator / integrable_real_indicator
-    positive_integral_fst       ~>  positive_integral_fst'
-    positive_integral_fst_measurable ~> positive_integral_fst
-    positive_integral_snd_measurable ~> positive_integral_snd
+    positive_integral_fst       ~>  nn_integral_fst'
+    positive_integral_fst_measurable ~> nn_integral_fst
+    positive_integral_snd_measurable ~> nn_integral_snd
 
     integrable_fst_measurable   ~>
          integral_fst / integrable_fst / AE_integrable_fst
@@ -906,7 +913,7 @@
          integrable_has_integral_lebesgue_nonneg
 
     lebesgue_integral_real_affine  ~>
-         positive_integral_real_affine
+         nn_integral_real_affine
 
     has_integral_iff_positive_integral_lborel  ~>
          integral_has_integral_nonneg / integrable_has_integral_nonneg
@@ -921,13 +928,6 @@
     integral_cmul_indicator
     integral_real
 
-  - Renamed positive_integral to nn_integral:
-
-    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
-      positive_integral_positive ~> nn_integral_nonneg
-
-    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
-
   - Formalized properties about exponentially, Erlang, and normal
     distributed random variables.