--- a/NEWS Sun Feb 16 18:39:40 2014 +0100
+++ b/NEWS Sun Feb 16 18:39:41 2014 +0100
@@ -87,7 +87,6 @@
The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
"primrec_new", "primcorec", and "primcorecursive" command are now part of
"Main".
- INCOMPATIBILITY.
Theory renamings:
FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
Library/Wfrec.thy ~> Wfrec.thy
@@ -118,15 +117,32 @@
Library/BNF_Decl.thy
BNF_Examples/Misc_Primcorec.thy
BNF_Examples/Stream_Processor.thy
- Discontinued theory:
+ Discontinued theories:
BNF/BNF.thy
BNF/Equiv_Relations_More.thy
+ Renamed command:
+ wrap_free_constructors ~> free_constructors
+ INCOMPATIBILITY.
* Old datatype package:
* Generated constants "xxx_case" and "xxx_rec" have been renamed "case_xxx"
- and "rec_xxx".
+ and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
INCOMPATIBILITY.
+* The types "'a list" and "'a option", their set and map functions, and their
+ selectors are now produced using the new BNF-based datatype package.
+ Renamed constants:
+ Option.set ~> set_option
+ Option.map ~> map_option
+ Renamed theorems:
+ map_def ~> map_rec[abs_def]
+ Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
+ map.simps ~> list.map
+ hd.simps ~> list.sel(1)
+ tl.simps ~> list.sel(2-3)
+ the.simps ~> option.sel
+ INCOMPATIBILITY.
+
* New theory:
Cardinals/Ordinal_Arithmetic.thy
@@ -147,6 +163,8 @@
* Try0: Added 'algebra' and 'meson' to the set of proof methods.
+* Command renaming: enriched_type ~> functor. INCOMPATIBILITY.
+
* The symbol "\<newline>" may be used within char or string literals
to represent (Char Nibble0 NibbleA), i.e. ASCII newline.