NEWS
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