# HG changeset patch
# User blanchet
# Date 1392572381 -3600
# Node ID 8a54bf4a92cadb153c7f97f91704a8e6289c89b0
# Parent  1ddb2edf5ceb34bb16155d2189d624cb8a6149df
more NEWS

diff -r 1ddb2edf5ceb -r 8a54bf4a92ca NEWS
--- 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.