NEWS

--- a/NEWS	Tue Mar 03 17:05:18 2009 +0100
+++ b/NEWS	Wed Mar 04 10:47:20 2009 +0100
@@ -500,6 +500,9 @@
     Suc_Suc_eq                  ~> nat.inject
     Suc_not_Zero Zero_not_Suc   ~> nat.distinct
 
+* The option datatype has been moved to a new theory HOL/Option.thy.
+Renamed option_map to Option.map.
+
 * Library/Nat_Infinity: added addition, numeral syntax and more
 instantiations for algebraic structures.  Removed some duplicate
 theorems.  Changes in simp rules.  INCOMPATIBILITY.