changeset 71259 | 09aee7f5b447 |
parent 71166 | c9433e8e314e |
child 71264 | 0c454a5d125d |
--- a/NEWS Mon Dec 09 15:36:51 2019 +0000 +++ b/NEWS Mon Dec 09 16:13:36 2019 +0000 @@ -81,6 +81,9 @@ * Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) associates to the left now as is customary. +* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with +multiple colours and arbitrary exponents. + * Theory Complete_Lattices: renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf