| changeset 49739 | 13aa6d8268ec |
| parent 49738 | 1e1611fd32df |
| child 49770 | cf6a78acf445 |
--- a/NEWS Mon Oct 08 11:37:03 2012 +0200 +++ b/NEWS Mon Oct 08 12:03:49 2012 +0200 @@ -62,6 +62,8 @@ *** HOL *** +* Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY. + * Class "comm_monoid_diff" formalises properties of bounded subtraction, with natural numbers and multisets as typical instances.