Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
authoreberlm
Tue Jan 05 15:38:37 2016 +0100 (2016-01-05)
changeset 62060b75764fc4c35
parent 62059 2da6f4945295
child 62063 b921b251f91f
child 62065 1546a042e87b
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Jan 05 14:25:12 2016 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Jan 05 15:38:37 2016 +0100
     1.3 @@ -6,6 +6,13 @@
     1.4  Contributions to Isabelle2016
     1.5  -----------------------------
     1.6  
     1.7 +* Winter 2015: Manuel Eberl, TUM
     1.8 +  The radius of convergence of power series and various summability tests.
     1.9 +  Harmonic numbers and the Euler–Mascheroni constant.
    1.10 +  The Generalised Binomial Theorem.
    1.11 +  The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and 
    1.12 +  their most important properties.
    1.13 +
    1.14  * Autumn 2015: Florian Haftmann, TUM
    1.15    Rewrite definitions for global interpretations and sublocale
    1.16    declarations.
     2.1 --- a/NEWS	Tue Jan 05 14:25:12 2016 +0100
     2.2 +++ b/NEWS	Tue Jan 05 15:38:37 2016 +0100
     2.3 @@ -642,6 +642,8 @@
     2.4  * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.
     2.5  Minor INCOMPATIBILITY, use 'function' instead.
     2.6  
     2.7 +* Library/Periodic_Fun: a locale that provides convenient lemmas for periodic functions
     2.8 +
     2.9  * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (=
    2.10  complex path integrals), Cauchy's integral theorem, winding numbers and
    2.11  Cauchy's integral formula, Liouville theorem, Fundamental Theorem of
    2.12 @@ -650,6 +652,11 @@
    2.13  * Multivariate_Analysis: Added topological concepts such as connected
    2.14  components, homotopic paths and the inside or outside of a set.
    2.15  
    2.16 +* Multivariate_Analysis: radius of convergence of power series and 
    2.17 +  various summability tests; Harmonic numbers and the Euler–Mascheroni constant;
    2.18 +  the Generalised Binomial Theorem; the complex and real Gamma/log-Gamma/Digamma/
    2.19 +  Polygamma functions and their most important properties;
    2.20 +
    2.21  * Data_Structures: new and growing session of standard data structures.
    2.22  
    2.23  * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.