--- a/NEWS Fri Apr 17 12:12:14 2015 +0200
+++ b/NEWS Fri Apr 17 13:01:09 2015 +0200
@@ -198,6 +198,15 @@
BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions
Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions
INCOMPATIBILITY.
+ - Lifting and Transfer setup for basic HOL types sum and prod
+ (also option) is now performed by the BNF package. Theories
+ Lifting_Sum, Lifting_Product and Lifting_Option from Main
+ became obsolete and were removed. Changed definitions of
+ the relators rel_prod and rel_sum (using inductive).
+ INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead
+ of rel_prod_def and rel_sum_def.
+ Minor INCOMPATIBILITY: (rarely used by name) transfer theorem
+ names changed (e.g. map_prod_transfer ~> prod.map_transfer).
* Old datatype package:
- The old 'datatype' command has been renamed 'old_datatype', and