NEWS
changeset 62086 1c0246456ab9
parent 62084 969119292e25
child 62097 634838f919e4
     1.1 --- a/NEWS	Thu Jan 07 14:37:17 2016 +0100
     1.2 +++ b/NEWS	Thu Jan 07 14:44:51 2016 +0100
     1.3 @@ -646,6 +646,9 @@
     1.4  * Library/Periodic_Fun: a locale that provides convenient lemmas for
     1.5  periodic functions.
     1.6  
     1.7 +* Library/Formal_Power_Series: proper definition of division (with remainder) 
     1.8 +for formal power series; instances for Euclidean Ring and GCD.
     1.9 +
    1.10  * HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    1.11  
    1.12  * HOL-Statespace: command 'statespace' uses mandatory qualifier for