diff -r 8a0fe5469ba0 -r 90ceace1e814 NEWS
--- a/NEWS	Sun Oct 23 16:44:17 2016 +0200
+++ b/NEWS	Mon Oct 24 13:50:12 2016 +0200
@@ -249,6 +249,8 @@
 
 *** HOL ***
 
+* Ported remaining theories of Old_Number_Theory and removed Old_Number_Theory.
+
 * Sligthly more standardized theorem names:
     sgn_times ~> sgn_mult
     sgn_mult' ~> Real_Vector_Spaces.sgn_mult