NEWS

--- a/NEWS	Fri Mar 06 20:29:37 2009 +0100
+++ b/NEWS	Fri Mar 06 20:30:16 2009 +0100
@@ -220,6 +220,9 @@
 
 *** HOL ***
 
+* Theory Library/Diagonalize.thy provides constructive version of
+Cantor's first diagonalization argument.
+
 * New predicate "strict_mono" classifies strict functions on partial orders.
 With strict functions on linear orders, reasoning about (in)equalities is
 facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less".