1.1 --- a/CONTRIBUTORS	Mon Sep 12 13:35:35 2011 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Sep 12 09:57:33 2011 -0400
     1.3 @@ -25,6 +25,11 @@
     1.4    Theory HOL/Library/Cset_Monad allows do notation for computable
     1.5    sets (cset) via the generic monad ad-hoc overloading facility.
     1.6  
     1.7 +* 2011: Johannes Hölzl, Armin Heller, TUM,
     1.8 +  and Bogdan Grechuk, Univeristy of Edinburgh
     1.9 +  Theory HOL/Library/Extended_Reals: real numbers extended with
    1.10 +  plus and minus infinity.
    1.11 +
    1.12  Contributions to Isabelle2011
    1.13  -----------------------------
    1.14  

     2.1 --- a/NEWS	Mon Sep 12 13:35:35 2011 +0200
     2.2 +++ b/NEWS	Mon Sep 12 09:57:33 2011 -0400
     2.3 @@ -224,9 +224,14 @@
     2.4  * Session HOL-Probability:
     2.5    - Caratheodory's extension lemma is now proved for ring_of_sets.
     2.6    - Infinite products of probability measures are now available.
     2.7 +  - Sigma closure is independent, if the generator is independent
     2.8    - Use extended reals instead of positive extended
     2.9      reals. INCOMPATIBILITY.
    2.10  
    2.11 +* Theory Library/Extended_Reals replaces now the positive extended reals
    2.12 +  found in probabilty thoery. This file is extended by
    2.13 +  Multivariate_Analysis/Extended_Real_Limits.
    2.14 +
    2.15  * Old 'recdef' package has been moved to theory Library/Old_Recdef,
    2.16  from where it must be imported explicitly.  INCOMPATIBILITY.
    2.17  
    2.18 @@ -408,6 +413,9 @@
    2.19    bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero
    2.20    LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]
    2.21  
    2.22 +* Theory Complex_Main: The definition of infinite series was generalized.
    2.23 +  Now it is defined on the type class {topological_spaces, comm_monoid_add}.
    2.24 +  Hence it is useable also for extended real numbers.
    2.25  
    2.26  *** Document preparation ***
    2.27