1.1 --- a/NEWS	Thu Dec 05 09:20:32 2013 +0100
     1.2 +++ b/NEWS	Thu Dec 05 09:23:59 2013 +0100
     1.3 @@ -79,6 +79,10 @@
     1.4  * Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
     1.5  instead of explicitly stating boundedness of sets.
     1.6  
     1.7 +* ccpo.admissible quantifies only over non-empty chains to allow
     1.8 +more syntax-directed proof rules; the case of the empty chain
     1.9 +shows up as additional case in fixpoint induction proofs.
    1.10 +INCOMPATIBILITY
    1.11  
    1.12  *** ML ***
    1.13