diff -r caf2637a28a9 -r 9a1c6587e6c1 NEWS
--- a/NEWS	Fri Apr 17 14:57:25 2015 +0200
+++ b/NEWS	Fri Apr 17 15:54:44 2015 +0200
@@ -51,6 +51,11 @@
 context, without implicit global state. Potential for accidental
 INCOMPATIBILITY, make sure that required theories are really imported.
 
+* Historical command-line terminator ";" is no longer accepted (and
+already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle
+update_semicolons" to remove obsolete semicolons from old theory
+sources.
+
 * Structural composition of proof methods (meth1; meth2) in Isar
 corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
 
@@ -77,8 +82,8 @@
 * Improved graphview panel with optional output of PNG or PDF, for
 display of 'thy_deps', 'locale_deps', 'class_deps' etc.
 
-* Command 'thy_deps' allows optional bounds, analogously to
-'class_deps'.
+* The commands 'thy_deps' and 'class_deps' allow optional bounds to
+restrict the visualized hierarchy.
 
 * Improved scheduling for asynchronous print commands (e.g. provers
 managed by the Sledgehammer panel) wrt. ongoing document processing.
@@ -141,9 +146,6 @@
 INCOMPATIBILITY, explicit instantiation sometimes needs to refer to
 different index.
 
-* Command "class_deps" takes optional sort arguments to constrain then
-resulting class hierarchy.
-
 * Lexical separation of signed and unsigned numerals: categories "num"
 and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence
 of numeral signs, particularly in expressions involving infix syntax
@@ -473,10 +475,6 @@
 look-and-feel, via internal class name or symbolic name as in the jEdit
 menu Global Options / Appearance.
 
-* Historical command-line terminator ";" is no longer accepted.  Minor
-INCOMPATIBILITY, use "isabelle update_semicolons" to remove obsolete
-semicolons from theory sources.
-
 * Support for Proof General and Isar TTY loop has been discontinued.
 Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.