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