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