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