summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 60114 | caf2637a28a9 |

parent 60111 | 3eaa39b3a0b7 |

child 60115 | 9a1c6587e6c1 |

1.1 --- a/NEWS Fri Apr 17 14:30:02 2015 +0200 1.2 +++ b/NEWS Fri Apr 17 14:57:25 2015 +0200 1.3 @@ -198,15 +198,15 @@ 1.4 BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions 1.5 Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions 1.6 INCOMPATIBILITY. 1.7 - - Lifting and Transfer setup for basic HOL types sum and prod 1.8 - (also option) is now performed by the BNF package. Theories 1.9 - Lifting_Sum, Lifting_Product and Lifting_Option from Main 1.10 - became obsolete and were removed. Changed definitions of 1.11 - the relators rel_prod and rel_sum (using inductive). 1.12 + - Lifting and Transfer setup for basic HOL types sum and prod (also 1.13 + option) is now performed by the BNF package. Theories Lifting_Sum, 1.14 + Lifting_Product and Lifting_Option from Main became obsolete and 1.15 + were removed. Changed definitions of the relators rel_prod and 1.16 + rel_sum (using inductive). 1.17 INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead 1.18 - of rel_prod_def and rel_sum_def. 1.19 - Minor INCOMPATIBILITY: (rarely used by name) transfer theorem 1.20 - names changed (e.g. map_prod_transfer ~> prod.map_transfer). 1.21 + of rel_prod_def and rel_sum_def. 1.22 + Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names 1.23 + changed (e.g. map_prod_transfer ~> prod.map_transfer). 1.24 1.25 * Old datatype package: 1.26 - The old 'datatype' command has been renamed 'old_datatype', and