Added formal power series updates to NEWS/CONTRIBUTORS
authorManuel Eberl <eberlm@in.tum.de>
Thu Jan 07 14:44:51 2016 +0100 (2016-01-07)
changeset 620861c0246456ab9
parent 62085 5b7758af429e
child 62088 8463e386eaec
Added formal power series updates to NEWS/CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Thu Jan 07 14:37:17 2016 +0100
     1.2 +++ b/CONTRIBUTORS	Thu Jan 07 14:44:51 2016 +0100
     1.3 @@ -16,6 +16,10 @@
     1.4    The Generalised Binomial Theorem.
     1.5    The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their
     1.6    most important properties.
     1.7 +  
     1.8 +* Autumn 2015: Manuel Eberl, TUM
     1.9 +  Proper definition of division (with remainder) for formal power series;
    1.10 +  Euclidean Ring and GCD instance for formal power series.
    1.11  
    1.12  * Autumn 2015: Florian Haftmann, TUM
    1.13    Rewrite definitions for global interpretations and sublocale declarations.
     2.1 --- a/NEWS	Thu Jan 07 14:37:17 2016 +0100
     2.2 +++ b/NEWS	Thu Jan 07 14:44:51 2016 +0100
     2.3 @@ -646,6 +646,9 @@
     2.4  * Library/Periodic_Fun: a locale that provides convenient lemmas for
     2.5  periodic functions.
     2.6  
     2.7 +* Library/Formal_Power_Series: proper definition of division (with remainder) 
     2.8 +for formal power series; instances for Euclidean Ring and GCD.
     2.9 +
    2.10  * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    2.11  
    2.12  * HOL-Statespace: command 'statespace' uses mandatory qualifier for