--- a/NEWS Fri Nov 08 17:34:37 2013 +0100
+++ b/NEWS Sat Nov 09 11:24:21 2013 +0100
@@ -201,7 +201,7 @@
* Lifting:
- parametrized correspondence relations are now supported:
- + parametricity theorems for the raw term can be specified in
+ + parametricity theorems for the raw term can be specified in
the command lift_definition, which allow us to generate stronger
transfer rules
+ setup_lifting generates stronger transfer rules if parametric
@@ -215,15 +215,15 @@
- ===> and --> are now local. The symbols can be introduced
by interpreting the locale lifting_syntax (typically in an
anonymous context)
- - Lifting/Transfer relevant parts of Library/Quotient_* are now in
+ - Lifting/Transfer relevant parts of Library/Quotient_* are now in
Main. Potential INCOMPATIBILITY
- new commands for restoring and deleting Lifting/Transfer context:
lifting_forget, lifting_update
- - the command print_quotmaps was renamed to print_quot_maps.
+ - the command print_quotmaps was renamed to print_quot_maps.
INCOMPATIBILITY
* Transfer:
- - better support for domains in Transfer: replace Domainp T
+ - better support for domains in Transfer: replace Domainp T
by the actual invariant in a transferred goal
- transfer rules can have as assumptions other transfer rules
- Experimental support for transferring from the raw level to the