--- a/ANNOUNCE Wed Jan 06 12:18:53 2016 +0100
+++ b/ANNOUNCE Wed Jan 06 16:17:50 2016 +0100
@@ -20,7 +20,8 @@
* HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer.
-* Many HOL library improvements, notably HOL-Multivariate_Analysis.
+* HOL library additions and improvements, notably HOL-Multivariate_Analysis,
+HOL-Probability, HOL-Data_Structures.
* Upgrade to Poly/ML 5.6 with debugger IDE support (Isabelle/ML and Standard
ML), per-thread profiling, native Windows version (32bit and 64bit).
--- a/CONTRIBUTORS Wed Jan 06 12:18:53 2016 +0100
+++ b/CONTRIBUTORS Wed Jan 06 16:17:50 2016 +0100
@@ -7,8 +7,8 @@
-----------------------------
* Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
- Proof of the central limit theorem: includes weak convergence, characteristic
- functions, and Levy's uniqueness and continuity theorem.
+ Proof of the central limit theorem: includes weak convergence,
+ characteristic functions, and Levy's uniqueness and continuity theorem.
* Winter 2015: Manuel Eberl, TUM
The radius of convergence of power series and various summability tests.
--- a/NEWS Wed Jan 06 12:18:53 2016 +0100
+++ b/NEWS Wed Jan 06 16:17:50 2016 +0100
@@ -646,30 +646,31 @@
* 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
-Algebra. Ported from HOL Light
-
-* Multivariate_Analysis: Added topological concepts such as connected
+* HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
+
+* HOL-Statespace: command 'statespace' uses mandatory qualifier for
+import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
+remove '!' and add '?' as required.
+
+* HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour
+integrals (= complex path integrals), Cauchy's integral theorem, winding
+numbers and Cauchy's integral formula, Liouville theorem, Fundamental
+Theorem of Algebra. Ported from HOL Light.
+
+* HOL-Multivariate_Analysis: 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
+* HOL-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.
-* Probability: The central limit theorem based on Levy's uniqueness and
-continuity theorems, weak convergence, and characterisitc functions.
-
-* Data_Structures: new and growing session of standard data structures.
-
-* Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
-
-* HOL-Statespace: command 'statespace' uses mandatory qualifier for
-import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
-remove '!' and add '?' as required.
+* HOL-Probability: The central limit theorem based on Levy's uniqueness
+and continuity theorems, weak convergence, and characterisitc functions.
+
+* HOL-Data_Structures: new and growing session of standard data
+structures.
*** ML ***