NEWS
authorkuncar
Mon May 04 14:16:20 2015 +0200 (2015-05-04)
changeset 602587364d4316a56
parent 60257 9ed816c033c5
child 60259 29f4e4366cb1
NEWS
NEWS
     1.1 --- a/NEWS	Mon May 04 21:58:35 2015 +0200
     1.2 +++ b/NEWS	Mon May 04 14:16:20 2015 +0200
     1.3 @@ -216,6 +216,11 @@
     1.4      of rel_prod_def and rel_sum_def.
     1.5      Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names
     1.6      changed (e.g. map_prod_transfer ~> prod.map_transfer).
     1.7 +  - Parametricity theorems for map functions, relators, set
     1.8 +    functions, constructors, case combinators, discriminators,
     1.9 +    selectors and (co)recursors are automatically proved and registred
    1.10 +    as transfer rules.
    1.11 +
    1.12  
    1.13  * Old datatype package:
    1.14    - The old 'datatype' command has been renamed 'old_datatype', and
    1.15 @@ -261,6 +266,13 @@
    1.16    - New option 'smt_statistics' to display statistics of the new 'smt'
    1.17      method, especially runtime statistics of Z3 proof reconstruction.
    1.18  
    1.19 +* Lifting
    1.20 +  - lift_definition command implements a workaround that allows us 
    1.21 +    to execute lifted constants that have as a return type 
    1.22 +    a datatype containing a subtype.
    1.23 +    This was a long time limitation in the area of code generation and
    1.24 +    lifting and the used workarounds were tedious.
    1.25 +
    1.26  * Command and antiquotation "value" provide different evaluation slots
    1.27  (again), where the previous strategy (NBE after ML) serves as default.
    1.28  Minor INCOMPATIBILITY.