NEWS
changeset 49189 3f85cd15a0cc
parent 49145 0ee5983e3d59
child 49190 e1e1d427747d
--- a/NEWS	Fri Sep 07 07:20:55 2012 +0200
+++ b/NEWS	Fri Sep 07 08:20:18 2012 +0200
@@ -41,6 +41,8 @@
 
 *** HOL ***
 
+* New combinator "Option.these" with type "'a option set => 'a option".
+
 * Renamed theory Library/List_Prefix to Library/Sublist.
 INCOMPATIBILITY.  Related changes are: