NEWS

--- a/NEWS	Sun Dec 15 15:10:14 2013 +0100
+++ b/NEWS	Sun Dec 15 15:10:16 2013 +0100
@@ -28,6 +28,9 @@
 
 *** HOL ***
 
+* Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin.
+INCOMPATBILITY.
+
 * Code generations are provided for make, fields, extend and truncate
 operations on records.