NEWS and CONTRIBUTORS
authorkuncar
Wed Oct 02 10:13:54 2013 +0300 (2013-10-02)
changeset 540218089e82833b6
parent 54020 0c7b5aa453bb
child 54022 aae0163c01ea
NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Oct 01 23:51:15 2013 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Oct 02 10:13:54 2013 +0300
     1.3 @@ -21,6 +21,12 @@
     1.4    Various improvements to BNF-based (co)datatype package, including
     1.5    "primrec_new" and "primcorec" commands and a compatibility layer.
     1.6  
     1.7 +* Spring and Summer 2013: Ondrej Kuncar, TUM
     1.8 +  Various improvments of Lifting and Transfer packages
     1.9 +
    1.10 +* Spring 2013: Brian Huffman, Galois Inc.
    1.11 +  Improvments of the Transfer package
    1.12 +  
    1.13  * Summer 2013: Daniel K├╝hlwein, ICIS, Radboud University Nijmegen
    1.14    Jasmin Blanchette, TUM
    1.15    Various improvements to MaSh, including a server mode.
     2.1 --- a/NEWS	Tue Oct 01 23:51:15 2013 +0200
     2.2 +++ b/NEWS	Wed Oct 02 10:13:54 2013 +0300
     2.3 @@ -169,6 +169,38 @@
     2.4      sets ~> set
     2.5  IMCOMPATIBILITY.
     2.6  
     2.7 +* Lifting:
     2.8 +  - parametrized correspondence relations are now supported:
     2.9 +    + parametricity theorems for the raw term can be specified in 
    2.10 +      the command lift_definition, which allow us to generate stronger
    2.11 +      transfer rules
    2.12 +    + setup_lifting generates stronger transfer rules if parametric
    2.13 +      correspondence relation can be generated
    2.14 +    + various new properties of the relator must be specified to support
    2.15 +      parametricity
    2.16 +    + parametricity theorem for the Quotient relation can be specified
    2.17 +  - setup_lifting generates domain rules for the Transfer package
    2.18 +  - stronger reflexivity prover of respectfulness theorems for type
    2.19 +    copies
    2.20 +  - ===> and --> are now local. The symbols can be introduced
    2.21 +    by interpreting the locale lifting_syntax (typically in an
    2.22 +    anonymous context)
    2.23 +  - Lifting/Transfer relevant parts of Library/Quotient_* are now in 
    2.24 +    Main. Potential INCOMPATIBILITY
    2.25 +  - new commands for restoring and deleting Lifting/Transfer context:
    2.26 +    lifting_forget, lifting_update
    2.27 +  - the command print_quotmaps was renamed to print_quot_maps. 
    2.28 +    INCOMPATIBILITY
    2.29 +
    2.30 +* Transfer:
    2.31 +  - better support for domains in Transfer: replace Domainp T 
    2.32 +    by the actual invariant in a transferred goal
    2.33 +  - transfer rules can have as assumptions other transfer rules
    2.34 +  - Experimental support for transferring from the raw level to the
    2.35 +    abstract level: Transfer.transferred attribute
    2.36 +  - Attribute version of the transfer method: untransferred attribute
    2.37 +  
    2.38 +
    2.39  * Function package: For mutually recursive functions f and g, separate
    2.40  cases rules f.cases and g.cases are generated instead of unusable
    2.41  f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,
    2.42 @@ -194,6 +226,9 @@
    2.43      expand_poly_eq ~> poly_eq_iff
    2.44  IMCOMPATIBILITY.
    2.45  
    2.46 +* New Library/FSet.thy: type of finite sets defined as a subtype of
    2.47 +  sets defined by Lifting/Transfer
    2.48 +
    2.49  * Reification and reflection:
    2.50    - Reification is now directly available in HOL-Main in structure
    2.51      "Reification".