tuned;
authorwenzelm
Fri Apr 17 15:54:44 2015 +0200 (2015-04-17)
changeset 601159a1c6587e6c1
parent 60114 caf2637a28a9
child 60116 5d90d301ad66
tuned;
NEWS
     1.1 --- a/NEWS	Fri Apr 17 14:57:25 2015 +0200
     1.2 +++ b/NEWS	Fri Apr 17 15:54:44 2015 +0200
     1.3 @@ -51,6 +51,11 @@
     1.4  context, without implicit global state. Potential for accidental
     1.5  INCOMPATIBILITY, make sure that required theories are really imported.
     1.6  
     1.7 +* Historical command-line terminator ";" is no longer accepted (and
     1.8 +already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle
     1.9 +update_semicolons" to remove obsolete semicolons from old theory
    1.10 +sources.
    1.11 +
    1.12  * Structural composition of proof methods (meth1; meth2) in Isar
    1.13  corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
    1.14  
    1.15 @@ -77,8 +82,8 @@
    1.16  * Improved graphview panel with optional output of PNG or PDF, for
    1.17  display of 'thy_deps', 'locale_deps', 'class_deps' etc.
    1.18  
    1.19 -* Command 'thy_deps' allows optional bounds, analogously to
    1.20 -'class_deps'.
    1.21 +* The commands 'thy_deps' and 'class_deps' allow optional bounds to
    1.22 +restrict the visualized hierarchy.
    1.23  
    1.24  * Improved scheduling for asynchronous print commands (e.g. provers
    1.25  managed by the Sledgehammer panel) wrt. ongoing document processing.
    1.26 @@ -141,9 +146,6 @@
    1.27  INCOMPATIBILITY, explicit instantiation sometimes needs to refer to
    1.28  different index.
    1.29  
    1.30 -* Command "class_deps" takes optional sort arguments to constrain then
    1.31 -resulting class hierarchy.
    1.32 -
    1.33  * Lexical separation of signed and unsigned numerals: categories "num"
    1.34  and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence
    1.35  of numeral signs, particularly in expressions involving infix syntax
    1.36 @@ -473,10 +475,6 @@
    1.37  look-and-feel, via internal class name or symbolic name as in the jEdit
    1.38  menu Global Options / Appearance.
    1.39  
    1.40 -* Historical command-line terminator ";" is no longer accepted.  Minor
    1.41 -INCOMPATIBILITY, use "isabelle update_semicolons" to remove obsolete
    1.42 -semicolons from theory sources.
    1.43 -
    1.44  * Support for Proof General and Isar TTY loop has been discontinued.
    1.45  Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
    1.46