summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | hoelzl |

Mon, 12 Sep 2011 09:57:33 -0400 | |

changeset 44901 | ed5ddf9fcc77 |

parent 44900 | 1a4ea8c5399a |

child 44902 | 9ba11d41cd1f |

adding NEWS and CONTRIBUTORS

CONTRIBUTORS | file | annotate | diff | comparison | revisions | |

NEWS | file | annotate | diff | comparison | revisions |

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