NEWS

--- a/NEWS	Sun Oct 12 16:31:43 2014 +0200
+++ b/NEWS	Sun Oct 12 17:05:34 2014 +0200
@@ -42,6 +42,12 @@
 
 *** HOL ***
 
+* Generalized and consolidated some theorems concerning divsibility:
+  dvd_reduce ~> dvd_add_triv_right_iff
+  dvd_plus_eq_right ~> dvd_add_right_iff
+  dvd_plus_eq_left ~> dvd_add_left_iff
+Minor INCOMPATIBILITY.
+
 * More foundational definition for predicate "even":
   even_def ~> even_iff_mod_2_eq_zero
 Minor INCOMPATIBILITY.