--- a/NEWS Thu Sep 12 22:10:17 2013 +0200
+++ b/NEWS Fri Sep 13 09:31:45 2013 +0200
@@ -225,7 +225,7 @@
- The whole reflection stack has been decomposed into conversions.
INCOMPATIBILITY.
-* Weaker precendence of syntax for big intersection and union on sets,
+* Stronger precedence of syntax for big intersection and union on sets,
in accordance with corresponding lattice operations. INCOMPATIBILITY.
* Nested case expressions are now translated in a separate check phase
@@ -260,8 +260,7 @@
* Locale hierarchy for abstract orderings and (semi)lattices.
-* Discontinued theory src/HOL/Library/Eval_Witness.
-INCOMPATIBILITY.
+* Discontinued theory src/HOL/Library/Eval_Witness. INCOMPATIBILITY.
* Discontinued obsolete src/HOL/IsaMakefile (considered legacy since
Isabelle2013). Use "isabelle build" to operate on Isabelle sessions.
@@ -278,9 +277,9 @@
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.
+* 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