NEWS

--- a/NEWS	Wed Oct 17 23:16:38 2007 +0200
+++ b/NEWS	Thu Oct 18 09:20:55 2007 +0200
@@ -562,6 +562,10 @@
 
 *** HOL ***
 
+* localized monotonicity predicate in theory "Orderings";
+integrated lemmas max_of_mono and min_of_mono with this predicate.
+INCOMPATIBILITY.
+
 * class "div" now inherits from class "times" rather than "type".
 INCOMPATIBILITY.