author | hoelzl |

Mon Sep 12 09:57:33 2011 -0400 (2011-09-12) | |

changeset 44901 | ed5ddf9fcc77 |

parent 44900 | 1a4ea8c5399a |

child 44902 | 9ba11d41cd1f |

adding NEWS and CONTRIBUTORS

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