--- 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.
--- 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