NEWS
changeset 62084 969119292e25
parent 62083 7582b39f51ed
child 62086 1c0246456ab9
child 62093 bd73a2279fcd
     1.1 --- a/NEWS	Wed Jan 06 12:18:53 2016 +0100
     1.2 +++ b/NEWS	Wed Jan 06 16:17:50 2016 +0100
     1.3 @@ -646,30 +646,31 @@
     1.4  * Library/Periodic_Fun: a locale that provides convenient lemmas for
     1.5  periodic functions.
     1.6  
     1.7 -* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (=
     1.8 -complex path integrals), Cauchy's integral theorem, winding numbers and
     1.9 -Cauchy's integral formula, Liouville theorem, Fundamental Theorem of
    1.10 -Algebra. Ported from HOL Light
    1.11 -
    1.12 -* Multivariate_Analysis: Added topological concepts such as connected
    1.13 +* HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    1.14 +
    1.15 +* HOL-Statespace: command 'statespace' uses mandatory qualifier for
    1.16 +import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
    1.17 +remove '!' and add '?' as required.
    1.18 +
    1.19 +* HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour
    1.20 +integrals (= complex path integrals), Cauchy's integral theorem, winding
    1.21 +numbers and Cauchy's integral formula, Liouville theorem, Fundamental
    1.22 +Theorem of Algebra. Ported from HOL Light.
    1.23 +
    1.24 +* HOL-Multivariate_Analysis: topological concepts such as connected
    1.25  components, homotopic paths and the inside or outside of a set.
    1.26  
    1.27 -* Multivariate_Analysis: radius of convergence of power series and 
    1.28 +* HOL-Multivariate_Analysis: radius of convergence of power series and
    1.29  various summability tests; Harmonic numbers and the Euler–Mascheroni
    1.30  constant; the Generalised Binomial Theorem; the complex and real
    1.31  Gamma/log-Gamma/Digamma/ Polygamma functions and their most important
    1.32  properties.
    1.33  
    1.34 -* Probability: The central limit theorem based on Levy's uniqueness and
    1.35 -continuity theorems, weak convergence, and characterisitc functions.
    1.36 -
    1.37 -* Data_Structures: new and growing session of standard data structures.
    1.38 -
    1.39 -* Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    1.40 -
    1.41 -* HOL-Statespace: command 'statespace' uses mandatory qualifier for
    1.42 -import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
    1.43 -remove '!' and add '?' as required.
    1.44 +* HOL-Probability: The central limit theorem based on Levy's uniqueness
    1.45 +and continuity theorems, weak convergence, and characterisitc functions.
    1.46 +
    1.47 +* HOL-Data_Structures: new and growing session of standard data
    1.48 +structures.
    1.49  
    1.50  
    1.51  *** ML ***