# HG changeset patch
# User wenzelm
# Date 1452093470 -3600
# Node ID 969119292e25360defb6e70e14f0fba1d246ff72
# Parent  7582b39f51ed7999db08cff12b4971889ee3b2dc
misc tuning for release;

diff -r 7582b39f51ed -r 969119292e25 ANNOUNCE
--- 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).
diff -r 7582b39f51ed -r 969119292e25 CONTRIBUTORS
--- 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.
diff -r 7582b39f51ed -r 969119292e25 NEWS
--- 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 ***