# HG changeset patch
# User Andreas Lochbihler
# Date 1386231839 -3600
# Node ID da88a625cce1af2d576c8d01a1f57e959645436c
# Parent  9061af4d5ebcf78fe4cf67515614ebba7b24593b
news

diff -r 9061af4d5ebc -r da88a625cce1 NEWS
--- a/NEWS	Thu Dec 05 09:20:32 2013 +0100
+++ b/NEWS	Thu Dec 05 09:23:59 2013 +0100
@@ -79,6 +79,10 @@
 * Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
 instead of explicitly stating boundedness of sets.
 
+* ccpo.admissible quantifies only over non-empty chains to allow
+more syntax-directed proof rules; the case of the empty chain
+shows up as additional case in fixpoint induction proofs.
+INCOMPATIBILITY
 
 *** ML ***