# HG changeset patch
# User wenzelm
# Date 1236173034 -3600
# Node ID 05d312f09a2545b963b84751533081ce7af162f4
# Parent  9d9145349d1902805011a0f929c8161a016eddd4
NEWS: renamed o2s to Option.set;

diff -r 9d9145349d19 -r 05d312f09a25 NEWS
--- a/NEWS	Wed Mar 04 13:42:23 2009 +0100
+++ b/NEWS	Wed Mar 04 14:23:54 2009 +0100
@@ -501,7 +501,7 @@
     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.
+Renamed option_map to Option.map, and o2s to Option.set.
 
 * Library/Nat_Infinity: added addition, numeral syntax and more
 instantiations for algebraic structures.  Removed some duplicate