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