misc tuning for release;
authorwenzelm
Tue Jan 05 15:53:17 2016 +0100 (2016-01-05)
changeset 62064d9874039786e
parent 62063 b921b251f91f
child 62066 4db2d39aa76c
child 62068 500f54190a3c
misc tuning for release;
ANNOUNCE
CONTRIBUTORS
NEWS
     1.1 --- a/ANNOUNCE	Tue Jan 05 15:45:29 2016 +0100
     1.2 +++ b/ANNOUNCE	Tue Jan 05 15:53:17 2016 +0100
     1.3 @@ -20,8 +20,7 @@
     1.4  
     1.5  * HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer.
     1.6  
     1.7 -* Many HOL library improvements, including advanced topological concepts and
     1.8 -integration theory ported from HOL Light.
     1.9 +* Many HOL library improvements, notably HOL-Multivariate_Analysis.
    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	Tue Jan 05 15:45:29 2016 +0100
     2.2 +++ b/CONTRIBUTORS	Tue Jan 05 15:53:17 2016 +0100
     2.3 @@ -8,40 +8,37 @@
     2.4  
     2.5  * Winter 2015: Manuel Eberl, TUM
     2.6    The radius of convergence of power series and various summability tests.
     2.7 -  Harmonic numbers and the Euler–Mascheroni constant.
     2.8 +  Harmonic numbers and the Euler-Mascheroni constant.
     2.9    The Generalised Binomial Theorem.
    2.10 -  The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and 
    2.11 -  their most important properties.
    2.12 +  The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their
    2.13 +  most important properties.
    2.14  
    2.15  * Autumn 2015: Florian Haftmann, TUM
    2.16 -  Rewrite definitions for global interpretations and sublocale
    2.17 -  declarations.
    2.18 +  Rewrite definitions for global interpretations and sublocale declarations.
    2.19  
    2.20  * Autumn 2015: Andreas Lochbihler
    2.21 -  Bourbaki-Witt fixpoint theorem for increasing functions on
    2.22 -  chain-complete partial orders.
    2.23 +  Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete
    2.24 +  partial orders.
    2.25  
    2.26  * Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl
    2.27    A large number of additional binomial identities.
    2.28  
    2.29  * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel
    2.30 -  Isar subgoal command for proof structure within unstructured proof
    2.31 -  scripts.
    2.32 +  Isar subgoal command for proof structure within unstructured proof scripts.
    2.33  
    2.34  * Summer 2015: Florian Haftmann, TUM
    2.35    Generic partial division in rings as inverse operation of multiplication.
    2.36  
    2.37  * Summer 2015: Manuel Eberl and Florian Haftmann, TUM
    2.38 -  Type class hierarchy with common algebraic notions of integral
    2.39 -  (semi)domains like units, associated elements and normalization
    2.40 -  wrt. units.
    2.41 +  Type class hierarchy with common algebraic notions of integral (semi)domains
    2.42 +  like units, associated elements and normalization wrt. units.
    2.43  
    2.44  * Summer 2015: Florian Haftmann, TUM
    2.45    Fundamentals of abstract type class for factorial rings.
    2.46  
    2.47  * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich
    2.48 -  Command to lift a BNF structure on the raw type to the abstract type
    2.49 -  for typedefs.
    2.50 +  Command to lift a BNF structure on the raw type to the abstract type for
    2.51 +  typedefs.
    2.52  
    2.53  
    2.54  Contributions to Isabelle2015
     3.1 --- a/NEWS	Tue Jan 05 15:45:29 2016 +0100
     3.2 +++ b/NEWS	Tue Jan 05 15:53:17 2016 +0100
     3.3 @@ -642,7 +642,8 @@
     3.4  * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.
     3.5  Minor INCOMPATIBILITY, use 'function' instead.
     3.6  
     3.7 -* Library/Periodic_Fun: a locale that provides convenient lemmas for periodic functions
     3.8 +* Library/Periodic_Fun: a locale that provides convenient lemmas for
     3.9 +periodic functions.
    3.10  
    3.11  * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (=
    3.12  complex path integrals), Cauchy's integral theorem, winding numbers and
    3.13 @@ -653,9 +654,10 @@
    3.14  components, homotopic paths and the inside or outside of a set.
    3.15  
    3.16  * Multivariate_Analysis: radius of convergence of power series and 
    3.17 -  various summability tests; Harmonic numbers and the Euler–Mascheroni constant;
    3.18 -  the Generalised Binomial Theorem; the complex and real Gamma/log-Gamma/Digamma/
    3.19 -  Polygamma functions and their most important properties;
    3.20 +various summability tests; Harmonic numbers and the Euler–Mascheroni
    3.21 +constant; the Generalised Binomial Theorem; the complex and real
    3.22 +Gamma/log-Gamma/Digamma/ Polygamma functions and their most important
    3.23 +properties.
    3.24  
    3.25  * Data_Structures: new and growing session of standard data structures.
    3.26