--- a/NEWS Fri Apr 17 14:30:02 2015 +0200
+++ b/NEWS Fri Apr 17 14:57:25 2015 +0200
@@ -198,15 +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).
+ - 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).
+ 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