NEWS
changeset 54021 8089e82833b6
parent 54010 5ac1495fed4e
child 54029 4edfd0fd5536
     1.1 --- a/NEWS	Tue Oct 01 23:51:15 2013 +0200
     1.2 +++ b/NEWS	Wed Oct 02 10:13:54 2013 +0300
     1.3 @@ -169,6 +169,38 @@
     1.4      sets ~> set
     1.5  IMCOMPATIBILITY.
     1.6  
     1.7 +* Lifting:
     1.8 +  - parametrized correspondence relations are now supported:
     1.9 +    + parametricity theorems for the raw term can be specified in 
    1.10 +      the command lift_definition, which allow us to generate stronger
    1.11 +      transfer rules
    1.12 +    + setup_lifting generates stronger transfer rules if parametric
    1.13 +      correspondence relation can be generated
    1.14 +    + various new properties of the relator must be specified to support
    1.15 +      parametricity
    1.16 +    + parametricity theorem for the Quotient relation can be specified
    1.17 +  - setup_lifting generates domain rules for the Transfer package
    1.18 +  - stronger reflexivity prover of respectfulness theorems for type
    1.19 +    copies
    1.20 +  - ===> and --> are now local. The symbols can be introduced
    1.21 +    by interpreting the locale lifting_syntax (typically in an
    1.22 +    anonymous context)
    1.23 +  - Lifting/Transfer relevant parts of Library/Quotient_* are now in 
    1.24 +    Main. Potential INCOMPATIBILITY
    1.25 +  - new commands for restoring and deleting Lifting/Transfer context:
    1.26 +    lifting_forget, lifting_update
    1.27 +  - the command print_quotmaps was renamed to print_quot_maps. 
    1.28 +    INCOMPATIBILITY
    1.29 +
    1.30 +* Transfer:
    1.31 +  - better support for domains in Transfer: replace Domainp T 
    1.32 +    by the actual invariant in a transferred goal
    1.33 +  - transfer rules can have as assumptions other transfer rules
    1.34 +  - Experimental support for transferring from the raw level to the
    1.35 +    abstract level: Transfer.transferred attribute
    1.36 +  - Attribute version of the transfer method: untransferred attribute
    1.37 +  
    1.38 +
    1.39  * Function package: For mutually recursive functions f and g, separate
    1.40  cases rules f.cases and g.cases are generated instead of unusable
    1.41  f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,
    1.42 @@ -194,6 +226,9 @@
    1.43      expand_poly_eq ~> poly_eq_iff
    1.44  IMCOMPATIBILITY.
    1.45  
    1.46 +* New Library/FSet.thy: type of finite sets defined as a subtype of
    1.47 +  sets defined by Lifting/Transfer
    1.48 +
    1.49  * Reification and reflection:
    1.50    - Reification is now directly available in HOL-Main in structure
    1.51      "Reification".