# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1452174291 -3600
# Node ID 1c0246456ab90c70d4d2912158bc35d4809a9dd5
# Parent  5b7758af429e154763118e1f2eb558cfd89abb21
Added formal power series updates to NEWS/CONTRIBUTORS

diff -r 5b7758af429e -r 1c0246456ab9 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Jan 07 14:37:17 2016 +0100
+++ b/CONTRIBUTORS	Thu Jan 07 14:44:51 2016 +0100
@@ -16,6 +16,10 @@
   The Generalised Binomial Theorem.
   The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their
   most important properties.
+  
+* Autumn 2015: Manuel Eberl, TUM
+  Proper definition of division (with remainder) for formal power series;
+  Euclidean Ring and GCD instance for formal power series.
 
 * Autumn 2015: Florian Haftmann, TUM
   Rewrite definitions for global interpretations and sublocale declarations.
diff -r 5b7758af429e -r 1c0246456ab9 NEWS
--- a/NEWS	Thu Jan 07 14:37:17 2016 +0100
+++ b/NEWS	Thu Jan 07 14:44:51 2016 +0100
@@ -646,6 +646,9 @@
 * Library/Periodic_Fun: a locale that provides convenient lemmas for
 periodic functions.
 
+* Library/Formal_Power_Series: proper definition of division (with remainder) 
+for formal power series; instances for Euclidean Ring and GCD.
+
 * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
 
 * HOL-Statespace: command 'statespace' uses mandatory qualifier for