NEWS

--- a/NEWS	Tue Jul 01 16:26:14 2014 +0200
+++ b/NEWS	Tue Jul 01 16:08:31 2014 +0100
@@ -205,6 +205,13 @@
 
 INCOMPATIBILITY.
 
+* Revisions to HOL/Number_Theory
+  - consolidated the proofs of the binomial theorem
+  - the function fib is again of type nat=>nat and not overloaded
+  - no more references to Old_Number_Theory in the HOL libraries (except the AFP)
+
+INCOMPATIBILITY.
+
 * Swapped orientation of facts image_comp and vimage_comp:
 
   image_compose ~> image_comp [symmetric]