corrected NEWS
authorhaftmann
Mon Oct 08 11:37:03 2012 +0200 (2012-10-08)
changeset 497381e1611fd32df
parent 49728 74f36dab2b62
child 49739 13aa6d8268ec
corrected NEWS
NEWS
     1.1 --- a/NEWS	Sun Oct 07 16:26:31 2012 +0200
     1.2 +++ b/NEWS	Mon Oct 08 11:37:03 2012 +0200
     1.3 @@ -62,13 +62,13 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* Class "comm_monoid_diff" formalised properties of bounded
     1.8 +* Class "comm_monoid_diff" formalises properties of bounded
     1.9  subtraction, with natural numbers and multisets as typical instances.
    1.10  
    1.11  * Theory "Library/Option_ord" provides instantiation of option type
    1.12  to lattice type classes.
    1.13  
    1.14 -* New combinator "Option.these" with type "'a option set => 'a option".
    1.15 +* New combinator "Option.these" with type "'a option set => 'a set".
    1.16  
    1.17  * Renamed theory Library/List_Prefix to Library/Sublist.
    1.18  INCOMPATIBILITY.  Related changes are: