# HG changeset patch
# User haftmann
# Date 1349689023 -7200
# Node ID 1e1611fd32df12e3df347398d07630add8abcd23
# Parent  74f36dab2b626d663ad7a8db70c046db133861b9
corrected NEWS

diff -r 74f36dab2b62 -r 1e1611fd32df NEWS
--- a/NEWS	Sun Oct 07 16:26:31 2012 +0200
+++ b/NEWS	Mon Oct 08 11:37:03 2012 +0200
@@ -62,13 +62,13 @@
 
 *** HOL ***
 
-* Class "comm_monoid_diff" formalised properties of bounded
+* Class "comm_monoid_diff" formalises properties of bounded
 subtraction, with natural numbers and multisets as typical instances.
 
 * Theory "Library/Option_ord" provides instantiation of option type
 to lattice type classes.
 
-* New combinator "Option.these" with type "'a option set => 'a option".
+* New combinator "Option.these" with type "'a option set => 'a set".
 
 * Renamed theory Library/List_Prefix to Library/Sublist.
 INCOMPATIBILITY.  Related changes are: