author | Andreas Lochbihler |
Thu, 05 Dec 2013 09:23:59 +0100 | |
changeset 54631 | da88a625cce1 |
parent 54630 | 9061af4d5ebc |
child 54632 | 7a14f831d02d |
--- 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 ***