author | wenzelm |

Wed Jan 06 16:17:50 2016 +0100 (2016-01-06) | |

changeset 62084 | 969119292e25 |

parent 62083 | 7582b39f51ed |

child 62085 | 5b7758af429e |

child 62087 | 44841d07ef1d |

child 62091 | c4d606633240 |

misc tuning for release;

ANNOUNCE | file | annotate | diff | revisions | |

CONTRIBUTORS | file | annotate | diff | revisions | |

NEWS | file | annotate | diff | revisions |

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