diff -r ec0fb01c6d50 -r 95c3ae4baba8 NEWS
--- a/NEWS	Sat Oct 01 12:03:27 2016 +0200
+++ b/NEWS	Sat Oct 01 17:16:35 2016 +0200
@@ -336,6 +336,12 @@
 eliminates the need to qualify any of those names in the presence of
 infix "mod" syntax. INCOMPATIBILITY.
 
+* Statements and proofs of Knaster-Tarski fixpoint combinators lfp/gfp
+have been clarified. The fixpoint properties are lfp_fixpoint, its
+symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items
+for the proof (lfp_lemma2 etc.) are no longer exported, but can be
+easily recovered by composition with eq_refl. Minor INCOMPATIBILITY.
+
 * Constant "surj" is a mere input abbreviation, to avoid hiding an
 equation in term output. Minor INCOMPATIBILITY.