NEWS

--- a/NEWS	Tue Dec 01 12:28:02 2015 +0100
+++ b/NEWS	Tue Dec 01 12:35:11 2015 +0100
@@ -581,6 +581,10 @@
     less_eq_multiset_def
     INCOMPATIBILITY
 
+* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the Bourbaki-Witt
+fixpoint theorem for increasing functions in chain-complete partial
+orders.
+
 * Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's
 integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light