# HG changeset patch
# User traytel
# Date 1429268469 -7200
# Node ID 3eaa39b3a0b7758f35fdd3fbad2521526a13f0fd
# Parent  82f355352490cf13a92572fe7be7ebbde37132f8
(low importance) NEWS

diff -r 82f355352490 -r 3eaa39b3a0b7 NEWS
--- 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