NEWS
changeset 60301 ff82ba1893c8
parent 60171 b3be7677461e
parent 60299 5ae2a2e74c93
child 60306 6b7c64ab8bd2
     1.1 --- a/NEWS	Sat May 23 22:13:24 2015 +0200
     1.2 +++ b/NEWS	Mon May 25 22:11:43 2015 +0200
     1.3 @@ -70,8 +70,9 @@
     1.4  by combining existing ones with their usual syntax. The "match" proof
     1.5  method provides basic fact/term matching in addition to
     1.6  premise/conclusion matching through Subgoal.focus, and binds fact names
     1.7 -from matches as well as term patterns within matches. See also
     1.8 -~~/src/HOL/Eisbach/Eisbach.thy and the included examples.
     1.9 +from matches as well as term patterns within matches. The Isabelle
    1.10 +documentation provides an entry "eisbach" for the Eisbach User Manual.
    1.11 +Sources and various examples are in ~~/src/HOL/Eisbach/.
    1.12  
    1.13  
    1.14  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.15 @@ -87,14 +88,14 @@
    1.16  marker, SideKick parser.
    1.17  
    1.18  * Document antiquotation @{cite} provides formal markup, which is
    1.19 -interpreted semi-formally based on .bib files that happen to be opened
    1.20 -in the editor (hyperlinks, completion etc.).
    1.21 +interpreted semi-formally based on .bib files that happen to be open in
    1.22 +the editor (hyperlinks, completion etc.).
    1.23  
    1.24  * Less waste of vertical space via negative line spacing (see Global
    1.25  Options / Text Area).
    1.26  
    1.27  * Improved graphview panel with optional output of PNG or PDF, for
    1.28 -display of 'thy_deps', 'locale_deps', 'class_deps' etc.
    1.29 +display of 'thy_deps', 'class_deps' etc.
    1.30  
    1.31  * The commands 'thy_deps' and 'class_deps' allow optional bounds to
    1.32  restrict the visualized hierarchy.
    1.33 @@ -139,6 +140,11 @@
    1.34  antiquotations need to observe the margin explicitly according to
    1.35  Thy_Output.string_of_margin. Minor INCOMPATIBILITY.
    1.36  
    1.37 +* Specification of 'document_files' in the session ROOT file is
    1.38 +mandatory for document preparation. The legacy mode with implicit
    1.39 +copying of the document/ directory is no longer supported. Minor
    1.40 +INCOMPATIBILITY.
    1.41 +
    1.42  
    1.43  *** Pure ***
    1.44  
    1.45 @@ -223,6 +229,10 @@
    1.46      of rel_prod_def and rel_sum_def.
    1.47      Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names
    1.48      changed (e.g. map_prod_transfer ~> prod.map_transfer).
    1.49 +  - Parametricity theorems for map functions, relators, set functions,
    1.50 +    constructors, case combinators, discriminators, selectors and
    1.51 +    (co)recursors are automatically proved and registered as transfer
    1.52 +    rules.
    1.53  
    1.54  * Old datatype package:
    1.55    - The old 'datatype' command has been renamed 'old_datatype', and
    1.56 @@ -268,6 +278,11 @@
    1.57    - New option 'smt_statistics' to display statistics of the new 'smt'
    1.58      method, especially runtime statistics of Z3 proof reconstruction.
    1.59  
    1.60 +* Lifting: command 'lift_definition' allows to execute lifted constants
    1.61 +that have as a return type a datatype containing a subtype. This
    1.62 +overcomes long-time limitations in the area of code generation and
    1.63 +lifting, and avoids tedious workarounds.
    1.64 +
    1.65  * Command and antiquotation "value" provide different evaluation slots
    1.66  (again), where the previous strategy (NBE after ML) serves as default.
    1.67  Minor INCOMPATIBILITY.