author | wenzelm |

Tue Jan 05 15:53:17 2016 +0100 (2016-01-05 ago) | |

changeset 62065 | d9874039786e |

parent 62064 | b921b251f91f |

child 62066 | 4db2d39aa76c |

child 62068 | 500f54190a3c |

misc tuning for release;

ANNOUNCE | file | annotate | diff | revisions | |

CONTRIBUTORS | file | annotate | diff | revisions | |

NEWS | file | annotate | diff | revisions |

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