--- 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.