misc tuning for release;
authorwenzelm
Wed Jan 06 16:17:50 2016 +0100 (2016-01-06)
changeset 62084969119292e25
parent 62083 7582b39f51ed
child 62085 5b7758af429e
child 62087 44841d07ef1d
child 62091 c4d606633240
misc tuning for release;
ANNOUNCE
CONTRIBUTORS
NEWS
     1.1 --- a/ANNOUNCE	Wed Jan 06 12:18:53 2016 +0100
     1.2 +++ b/ANNOUNCE	Wed Jan 06 16:17:50 2016 +0100
     1.3 @@ -20,7 +20,8 @@
     1.4  
     1.5  * HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer.
     1.6  
     1.7 -* Many HOL library improvements, notably HOL-Multivariate_Analysis.
     1.8 +* HOL library additions and improvements, notably HOL-Multivariate_Analysis,
     1.9 +HOL-Probability, HOL-Data_Structures.
    1.10  
    1.11  * Upgrade to Poly/ML 5.6 with debugger IDE support (Isabelle/ML and Standard
    1.12  ML), per-thread profiling, native Windows version (32bit and 64bit).
     2.1 --- a/CONTRIBUTORS	Wed Jan 06 12:18:53 2016 +0100
     2.2 +++ b/CONTRIBUTORS	Wed Jan 06 16:17:50 2016 +0100
     2.3 @@ -7,8 +7,8 @@
     2.4  -----------------------------
     2.5  
     2.6  * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
     2.7 -  Proof of the central limit theorem: includes weak convergence, characteristic
     2.8 -  functions, and Levy's uniqueness and continuity theorem.
     2.9 +  Proof of the central limit theorem: includes weak convergence,
    2.10 +  characteristic functions, and Levy's uniqueness and continuity theorem.
    2.11  
    2.12  * Winter 2015: Manuel Eberl, TUM
    2.13    The radius of convergence of power series and various summability tests.
     3.1 --- a/NEWS	Wed Jan 06 12:18:53 2016 +0100
     3.2 +++ b/NEWS	Wed Jan 06 16:17:50 2016 +0100
     3.3 @@ -646,30 +646,31 @@
     3.4  * Library/Periodic_Fun: a locale that provides convenient lemmas for
     3.5  periodic functions.
     3.6  
     3.7 -* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (=
     3.8 -complex path integrals), Cauchy's integral theorem, winding numbers and
     3.9 -Cauchy's integral formula, Liouville theorem, Fundamental Theorem of
    3.10 -Algebra. Ported from HOL Light
    3.11 -
    3.12 -* Multivariate_Analysis: Added topological concepts such as connected
    3.13 +* HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    3.14 +
    3.15 +* HOL-Statespace: command 'statespace' uses mandatory qualifier for
    3.16 +import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
    3.17 +remove '!' and add '?' as required.
    3.18 +
    3.19 +* HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour
    3.20 +integrals (= complex path integrals), Cauchy's integral theorem, winding
    3.21 +numbers and Cauchy's integral formula, Liouville theorem, Fundamental
    3.22 +Theorem of Algebra. Ported from HOL Light.
    3.23 +
    3.24 +* HOL-Multivariate_Analysis: topological concepts such as connected
    3.25  components, homotopic paths and the inside or outside of a set.
    3.26  
    3.27 -* Multivariate_Analysis: radius of convergence of power series and 
    3.28 +* HOL-Multivariate_Analysis: radius of convergence of power series and
    3.29  various summability tests; Harmonic numbers and the Euler–Mascheroni
    3.30  constant; the Generalised Binomial Theorem; the complex and real
    3.31  Gamma/log-Gamma/Digamma/ Polygamma functions and their most important
    3.32  properties.
    3.33  
    3.34 -* Probability: The central limit theorem based on Levy's uniqueness and
    3.35 -continuity theorems, weak convergence, and characterisitc functions.
    3.36 -
    3.37 -* Data_Structures: new and growing session of standard data structures.
    3.38 -
    3.39 -* Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    3.40 -
    3.41 -* HOL-Statespace: command 'statespace' uses mandatory qualifier for
    3.42 -import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
    3.43 -remove '!' and add '?' as required.
    3.44 +* HOL-Probability: The central limit theorem based on Levy's uniqueness
    3.45 +and continuity theorems, weak convergence, and characterisitc functions.
    3.46 +
    3.47 +* HOL-Data_Structures: new and growing session of standard data
    3.48 +structures.
    3.49  
    3.50  
    3.51  *** ML ***