# HG changeset patch
# User hoelzl
# Date 1315835853 14400
# Node ID ed5ddf9fcc7710f435ce18e969e705eedb93ac6b
# Parent  1a4ea8c5399a15f5c640fe1c8165f31f945c2d00
adding NEWS and CONTRIBUTORS

diff -r 1a4ea8c5399a -r ed5ddf9fcc77 CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Sep 12 13:35:35 2011 +0200
+++ b/CONTRIBUTORS	Mon Sep 12 09:57:33 2011 -0400
@@ -25,6 +25,11 @@
   Theory HOL/Library/Cset_Monad allows do notation for computable
   sets (cset) via the generic monad ad-hoc overloading facility.
 
+* 2011: Johannes Hölzl, Armin Heller, TUM,
+  and Bogdan Grechuk, Univeristy of Edinburgh
+  Theory HOL/Library/Extended_Reals: real numbers extended with
+  plus and minus infinity.
+
 Contributions to Isabelle2011
 -----------------------------
 
diff -r 1a4ea8c5399a -r ed5ddf9fcc77 NEWS
--- a/NEWS	Mon Sep 12 13:35:35 2011 +0200
+++ b/NEWS	Mon Sep 12 09:57:33 2011 -0400
@@ -224,9 +224,14 @@
 * Session HOL-Probability:
   - Caratheodory's extension lemma is now proved for ring_of_sets.
   - Infinite products of probability measures are now available.
+  - Sigma closure is independent, if the generator is independent
   - Use extended reals instead of positive extended
     reals. INCOMPATIBILITY.
 
+* Theory Library/Extended_Reals replaces now the positive extended reals
+  found in probabilty thoery. This file is extended by
+  Multivariate_Analysis/Extended_Real_Limits.
+
 * Old 'recdef' package has been moved to theory Library/Old_Recdef,
 from where it must be imported explicitly.  INCOMPATIBILITY.
 
@@ -408,6 +413,9 @@
   bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero
   LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]
 
+* Theory Complex_Main: The definition of infinite series was generalized.
+  Now it is defined on the type class {topological_spaces, comm_monoid_add}.
+  Hence it is useable also for extended real numbers.
 
 *** Document preparation ***