1.1 --- a/NEWS	Wed Sep 11 11:07:39 2013 +0200
     1.2 +++ b/NEWS	Wed Sep 11 11:08:48 2013 +0200
     1.3 @@ -247,8 +247,7 @@
     1.4  
     1.5  * Locale hierarchy for abstract orderings and (semi)lattices.
     1.6  
     1.7 -* Discontinued theory src/HOL/Library/Eval_Witness.
     1.8 -INCOMPATIBILITY.
     1.9 +* Discontinued theory src/HOL/Library/Eval_Witness.  INCOMPATIBILITY.
    1.10  
    1.11  * Discontinued obsolete src/HOL/IsaMakefile (considered legacy since
    1.12  Isabelle2013).  Use "isabelle build" to operate on Isabelle sessions.
    1.13 @@ -265,9 +264,9 @@
    1.14  Code_Target_Nat and Code_Target_Numeral.  See the tutorial on code
    1.15  generation for details.  INCOMPATIBILITY.
    1.16  
    1.17 -* Complete_Partial_Order.admissible is defined outside the type 
    1.18 -class ccpo, but with mandatory prefix ccpo. Admissibility theorems
    1.19 -lose the class predicate assumption or sort constraint when possible.
    1.20 +* Complete_Partial_Order.admissible is defined outside the type class
    1.21 +ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the
    1.22 +class predicate assumption or sort constraint when possible.
    1.23  INCOMPATIBILITY.
    1.24  
    1.25  * Introduce type class "conditionally_complete_lattice": Like a