summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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