--- a/NEWS Tue Dec 10 01:06:39 2019 +0100
+++ b/NEWS Tue Dec 10 01:06:39 2019 +0100
@@ -59,6 +59,11 @@
*** HOL ***
+* Improvements of the "lift_bnf" command:
+ - Add support for quotient types.
+ - Generate transfer rules for the lifted map/set/rel/pred
+ constants (theorems "<type>.<constant>_transfer_raw").
+
* Term_XML.Encode/Decode.term uses compact representation of Const
"typargs" from the given declaration environment. This also makes more
sense for translations to lambda-calculi with explicit polymorphism.