# HG changeset patch
# User wenzelm
# Date 1452005129 -3600
# Node ID b921b251f91f0188c1361088b429ba86938b1f0c
# Parent  b75764fc4c350989d2b8e457e978d00079686ba1# Parent  ee610059b0e9900c39f65eede93e1cbab11abc1c
merged

diff -r ee610059b0e9 -r b921b251f91f CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Jan 05 15:40:25 2016 +0100
+++ b/CONTRIBUTORS	Tue Jan 05 15:45:29 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.
diff -r ee610059b0e9 -r b921b251f91f NEWS
--- a/NEWS	Tue Jan 05 15:40:25 2016 +0100
+++ b/NEWS	Tue Jan 05 15:45:29 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.