--- 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
-----------------------------
--- 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 ***