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

author | wenzelm |

Tue, 05 Jan 2016 15:53:17 +0100 | |

changeset 62064 | d9874039786e |

parent 62063 | b921b251f91f |

child 62066 | 4db2d39aa76c |

child 62068 | 500f54190a3c |

misc tuning for release;

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

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

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

--- a/ANNOUNCE Tue Jan 05 15:45:29 2016 +0100 +++ b/ANNOUNCE Tue Jan 05 15:53:17 2016 +0100 @@ -20,8 +20,7 @@ * HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer. -* Many HOL library improvements, including advanced topological concepts and -integration theory ported from HOL Light. +* Many HOL library improvements, notably HOL-Multivariate_Analysis. * 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 Tue Jan 05 15:45:29 2016 +0100 +++ b/CONTRIBUTORS Tue Jan 05 15:53:17 2016 +0100 @@ -8,40 +8,37 @@ * Winter 2015: Manuel Eberl, TUM The radius of convergence of power series and various summability tests. - Harmonic numbers and the Eulerâ€“Mascheroni constant. + 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. + The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their + most important properties. * Autumn 2015: Florian Haftmann, TUM - Rewrite definitions for global interpretations and sublocale - declarations. + Rewrite definitions for global interpretations and sublocale declarations. * Autumn 2015: Andreas Lochbihler - Bourbaki-Witt fixpoint theorem for increasing functions on - chain-complete partial orders. + Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete + partial orders. * Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl A large number of additional binomial identities. * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel - Isar subgoal command for proof structure within unstructured proof - scripts. + Isar subgoal command for proof structure within unstructured proof scripts. * Summer 2015: Florian Haftmann, TUM Generic partial division in rings as inverse operation of multiplication. * Summer 2015: Manuel Eberl and Florian Haftmann, TUM - Type class hierarchy with common algebraic notions of integral - (semi)domains like units, associated elements and normalization - wrt. units. + Type class hierarchy with common algebraic notions of integral (semi)domains + like units, associated elements and normalization wrt. units. * Summer 2015: Florian Haftmann, TUM Fundamentals of abstract type class for factorial rings. * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich - Command to lift a BNF structure on the raw type to the abstract type - for typedefs. + Command to lift a BNF structure on the raw type to the abstract type for + typedefs. Contributions to Isabelle2015

--- a/NEWS Tue Jan 05 15:45:29 2016 +0100 +++ b/NEWS Tue Jan 05 15:53:17 2016 +0100 @@ -642,7 +642,8 @@ * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command. Minor INCOMPATIBILITY, use 'function' instead. -* Library/Periodic_Fun: a locale that provides convenient lemmas for periodic functions +* 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 @@ -653,9 +654,10 @@ components, homotopic paths and the inside or outside of a set. * 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; +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. * Data_Structures: new and growing session of standard data structures.