tuned whitespace;
authorwenzelm
Sat, 09 Nov 2013 11:24:21 +0100
changeset 5526672254819befd
parent 55265 750561986828
child 55267 4fac53028f87
tuned whitespace;
NEWS
     1.1 --- a/NEWS	Fri Nov 08 17:34:37 2013 +0100
     1.2 +++ b/NEWS	Sat Nov 09 11:24:21 2013 +0100
     1.3 @@ -201,7 +201,7 @@
     1.4  
     1.5  * Lifting:
     1.6    - parametrized correspondence relations are now supported:
     1.7 -    + parametricity theorems for the raw term can be specified in 
     1.8 +    + parametricity theorems for the raw term can be specified in
     1.9        the command lift_definition, which allow us to generate stronger
    1.10        transfer rules
    1.11      + setup_lifting generates stronger transfer rules if parametric
    1.12 @@ -215,15 +215,15 @@
    1.13    - ===> and --> are now local. The symbols can be introduced
    1.14      by interpreting the locale lifting_syntax (typically in an
    1.15      anonymous context)
    1.16 -  - Lifting/Transfer relevant parts of Library/Quotient_* are now in 
    1.17 +  - Lifting/Transfer relevant parts of Library/Quotient_* are now in
    1.18      Main. Potential INCOMPATIBILITY
    1.19    - new commands for restoring and deleting Lifting/Transfer context:
    1.20      lifting_forget, lifting_update
    1.21 -  - the command print_quotmaps was renamed to print_quot_maps. 
    1.22 +  - the command print_quotmaps was renamed to print_quot_maps.
    1.23      INCOMPATIBILITY
    1.24  
    1.25  * Transfer:
    1.26 -  - better support for domains in Transfer: replace Domainp T 
    1.27 +  - better support for domains in Transfer: replace Domainp T
    1.28      by the actual invariant in a transferred goal
    1.29    - transfer rules can have as assumptions other transfer rules
    1.30    - Experimental support for transferring from the raw level to the