# HG changeset patch # User wenzelm # Date 1430770295 -7200 # Node ID e0c3e11e9bea53656fdd1a258ac66c2e74390582 # Parent 2795bd5e502ed0601759332e68389f3995b40130 tuned; diff -r 2795bd5e502e -r e0c3e11e9bea CONTRIBUTORS --- a/CONTRIBUTORS Mon May 04 16:12:37 2015 +0200 +++ b/CONTRIBUTORS Mon May 04 22:11:35 2015 +0200 @@ -10,8 +10,8 @@ The Eisbach proof method language and "match" method. * Winter 2014 and Spring 2015: Ondrej Kuncar, TUM - Extension of lift_definition to execute lifted functions that have as a return type - a datatype containing a subtype. + Extension of lift_definition to execute lifted functions that have as a + return type a datatype containing a subtype. * March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII, and Dmitriy Traytel, TUM diff -r 2795bd5e502e -r e0c3e11e9bea NEWS --- a/NEWS Mon May 04 16:12:37 2015 +0200 +++ b/NEWS Mon May 04 22:11:35 2015 +0200 @@ -216,11 +216,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 registred - as transfer rules. - + - 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 @@ -266,12 +265,10 @@ - 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. +* 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.