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

author | eberlm |

Tue, 05 Jan 2016 15:38:37 +0100 | |

changeset 62060 | b75764fc4c35 |

parent 62059 | 2da6f4945295 |

child 62063 | b921b251f91f |

child 62065 | 1546a042e87b |

Added summability/Gamma/etc. to NEWS and CONTRIBUTORS

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

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

--- a/CONTRIBUTORS Tue Jan 05 14:25:12 2016 +0100 +++ b/CONTRIBUTORS Tue Jan 05 15:38:37 2016 +0100 @@ -6,6 +6,13 @@ Contributions to Isabelle2016 ----------------------------- +* Winter 2015: Manuel Eberl, TUM + The radius of convergence of power series and various summability tests. + Harmonic numbers and the Eulerâ€“Mascheroni constant. + The Generalised Binomial Theorem. + The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and + their most important properties. + * Autumn 2015: Florian Haftmann, TUM Rewrite definitions for global interpretations and sublocale declarations.

--- a/NEWS Tue Jan 05 14:25:12 2016 +0100 +++ b/NEWS Tue Jan 05 15:38:37 2016 +0100 @@ -642,6 +642,8 @@ * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command. Minor INCOMPATIBILITY, use 'function' instead. +* Library/Periodic_Fun: a locale that provides convenient lemmas for periodic functions + * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals), Cauchy's integral theorem, winding numbers and Cauchy's integral formula, Liouville theorem, Fundamental Theorem of @@ -650,6 +652,11 @@ * Multivariate_Analysis: Added topological concepts such as connected components, homotopic paths and the inside or outside of a set. +* Multivariate_Analysis: radius of convergence of power series and + various summability tests; Harmonic numbers and the Eulerâ€“Mascheroni constant; + the Generalised Binomial Theorem; the complex and real Gamma/log-Gamma/Digamma/ + Polygamma functions and their most important properties; + * Data_Structures: new and growing session of standard data structures. * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.