NEWS

--- a/NEWS	Wed Feb 18 22:46:47 2015 +0100
+++ b/NEWS	Wed Feb 18 22:46:48 2015 +0100
@@ -68,6 +68,11 @@
 
 *** HOL ***
 
+* Eliminated fact duplicates:
+  mult_less_imp_less_right ~> mult_right_less_imp_less
+  mult_less_imp_less_left ~> mult_left_less_imp_less
+Minor INCOMPATIBILITY.
+
 * Fact consolidation: even_less_0_iff is subsumed by
 double_add_less_zero_iff_single_add_less_zero (simp by default anyway).