--- a/NEWS Wed Feb 19 16:32:37 2014 +0100
+++ b/NEWS Wed Feb 19 16:33:11 2014 +0100
@@ -128,22 +128,24 @@
wrap_free_constructors ~> free_constructors
INCOMPATIBILITY.
-* Old datatype package:
+* Old and new (co)datatype packages:
* Generated constants "xxx_case" and "xxx_rec" have been renamed "case_xxx"
and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
INCOMPATIBILITY.
* The types "'a list" and "'a option", their set and map functions, their
- relators, and their selectors are now produced using the new BNF-based datatype
- package.
+ relators, and their selectors are now produced using the new BNF-based
+ datatype package.
Renamed constants:
Option.set ~> set_option
Option.map ~> map_option
option_rel ~> rel_option
Renamed theorems:
+ set_def ~> set_rec[abs_def]
map_def ~> map_rec[abs_def]
Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
list_all2_def ~> list_all2_iff
+ set.simps ~> set_simps (or the slightly different "list.set")
map.simps ~> list.map
hd.simps ~> list.sel(1)
tl.simps ~> list.sel(2-3)