--- 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: