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