summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 06 Jan 2016 16:17:50 +0100 | |

changeset 62084 | 969119292e25 |

parent 62083 | 7582b39f51ed |

child 62085 | 5b7758af429e |

child 62087 | 44841d07ef1d |

child 62091 | c4d606633240 |

misc tuning for release;

ANNOUNCE | file | annotate | diff | comparison | revisions | |

CONTRIBUTORS | file | annotate | diff | comparison | revisions | |

NEWS | file | annotate | diff | comparison | revisions |

--- 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).

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

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