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