# HG changeset patch
# User kuncar
# Date 1430741780 -7200
# Node ID 7364d4316a5691fc1d45c85f960796c76bd689c6
# Parent  9ed816c033c5039e6dc7400269fc004abe37858e
NEWS

diff -r 9ed816c033c5 -r 7364d4316a56 NEWS
--- a/NEWS	Mon May 04 21:58:35 2015 +0200
+++ b/NEWS	Mon May 04 14:16:20 2015 +0200
@@ -216,6 +216,11 @@
     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 registred
+    as transfer rules.
+
 
 * Old datatype package:
   - The old 'datatype' command has been renamed 'old_datatype', and
@@ -261,6 +266,13 @@
   - New option 'smt_statistics' to display statistics of the new 'smt'
     method, especially runtime statistics of Z3 proof reconstruction.
 
+* Lifting
+  - lift_definition command implements a workaround that allows us 
+    to execute lifted constants that have as a return type 
+    a datatype containing a subtype.
+    This was a long time limitation in the area of code generation and
+    lifting and the used workarounds were tedious.
+
 * Command and antiquotation "value" provide different evaluation slots
 (again), where the previous strategy (NBE after ML) serves as default.
 Minor INCOMPATIBILITY.