tuned;
authorwenzelm
Mon May 04 22:11:35 2015 +0200 (2015-05-04)
changeset 60261e0c3e11e9bea
parent 60260 2795bd5e502e
child 60262 1470c081b49c
tuned;
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Mon May 04 16:12:37 2015 +0200
     1.2 +++ b/CONTRIBUTORS	Mon May 04 22:11:35 2015 +0200
     1.3 @@ -10,8 +10,8 @@
     1.4    The Eisbach proof method language and "match" method.
     1.5  
     1.6  * Winter 2014 and Spring 2015: Ondrej Kuncar, TUM
     1.7 -  Extension of lift_definition to execute lifted functions that have as a return type 
     1.8 -  a datatype containing a subtype. 
     1.9 +  Extension of lift_definition to execute lifted functions that have as a
    1.10 +  return type a datatype containing a subtype.
    1.11  
    1.12  * March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII,
    1.13    and Dmitriy Traytel, TUM
     2.1 --- a/NEWS	Mon May 04 16:12:37 2015 +0200
     2.2 +++ b/NEWS	Mon May 04 22:11:35 2015 +0200
     2.3 @@ -216,11 +216,10 @@
     2.4      of rel_prod_def and rel_sum_def.
     2.5      Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names
     2.6      changed (e.g. map_prod_transfer ~> prod.map_transfer).
     2.7 -  - Parametricity theorems for map functions, relators, set
     2.8 -    functions, constructors, case combinators, discriminators,
     2.9 -    selectors and (co)recursors are automatically proved and registred
    2.10 -    as transfer rules.
    2.11 -
    2.12 +  - Parametricity theorems for map functions, relators, set functions,
    2.13 +    constructors, case combinators, discriminators, selectors and
    2.14 +    (co)recursors are automatically proved and registered as transfer
    2.15 +    rules.
    2.16  
    2.17  * Old datatype package:
    2.18    - The old 'datatype' command has been renamed 'old_datatype', and
    2.19 @@ -266,12 +265,10 @@
    2.20    - New option 'smt_statistics' to display statistics of the new 'smt'
    2.21      method, especially runtime statistics of Z3 proof reconstruction.
    2.22  
    2.23 -* Lifting
    2.24 -  - lift_definition command implements a workaround that allows us 
    2.25 -    to execute lifted constants that have as a return type 
    2.26 -    a datatype containing a subtype.
    2.27 -    This was a long time limitation in the area of code generation and
    2.28 -    lifting and the used workarounds were tedious.
    2.29 +* Lifting: command 'lift_definition' allows to execute lifted constants
    2.30 +that have as a return type a datatype containing a subtype. This
    2.31 +overcomes long-time limitations in the area of code generation and
    2.32 +lifting, and avoids tedious workarounds.
    2.33  
    2.34  * Command and antiquotation "value" provide different evaluation slots
    2.35  (again), where the previous strategy (NBE after ML) serves as default.