diff -r 1cb7d3c0cf31 -r 735e078a64e7 NEWS
--- a/NEWS	Mon Sep 02 16:28:11 2013 +0200
+++ b/NEWS	Mon Sep 02 17:14:35 2013 +0200
@@ -265,6 +265,11 @@
 Code_Target_Nat and Code_Target_Numeral.  See the tutorial on code
 generation for details.  INCOMPATIBILITY.
 
+* Complete_Partial_Order.admissible is defined outside the type 
+class ccpo, but with mandatory prefix ccpo. Admissibility theorems
+lose the class predicate assumption or sort constraint when possible.
+INCOMPATIBILITY.
+
 * Introduce type class "conditionally_complete_lattice": Like a
 complete lattice but does not assume the existence of the top and
 bottom elements.  Allows to generalize some lemmas about reals and