# HG changeset patch
# User blanchet
# Date 1377857197 -7200
# Node ID 221ff2b39a3533c9149589d468fd0a5dd783e466
# Parent  45f13517693a1600f8a2d8d4e4c2e00c21f2961b
updated news/contributors with BNF stuff

diff -r 45f13517693a -r 221ff2b39a35 CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Aug 30 12:06:11 2013 +0200
+++ b/CONTRIBUTORS	Fri Aug 30 12:06:37 2013 +0200
@@ -6,8 +6,12 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and Jasmin Blanchette, TUM
+  Various improvements to BNF-based (co)datatype package, including a
+  "primrec_new" command and a compatibility layer.
+
 * Summer 2013: Christian Sternagel, JAIST
-  Improved support for adhoc overloading of constants, including
+  Improved support for ad hoc overloading of constants, including
   documentation and examples.
 
 * May 2013: Florian Haftmann, TUM
diff -r 45f13517693a -r 221ff2b39a35 NEWS
--- a/NEWS	Fri Aug 30 12:06:11 2013 +0200
+++ b/NEWS	Fri Aug 30 12:06:37 2013 +0200
@@ -141,7 +141,7 @@
 
 *** HOL ***
 
-* Improved support for adhoc overloading of constants (see also
+* Improved support for ad hoc overloading of constants (see also
 isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).
 
 * Attibute 'code': 'code' now declares concrete and abstract code
@@ -156,6 +156,20 @@
   See the isar-ref manual for syntax diagrams, and the HOL theories
   for examples.
 
+* HOL/BNF:
+  - Various improvements to BNF-based (co)datatype package, including a
+    "primrec_new" command, a "datatype_compat" command, and
+    documentation. See "datatypes.pdf" for details.
+  - Renamed keywords:
+    data ~> datatype_new
+    codata ~> codatatype
+    bnf_def ~> bnf
+  - Renamed many generated theorems, including
+    map_comp' ~> map_comp
+    map_id' ~> map_id
+    set_map' ~> set_map
+IMCOMPATIBILITY.
+
 * Library/Polynomial.thy:
   - Use lifting for primitive definitions.
   - Explicit conversions from and to lists of coefficients, used for
@@ -166,7 +180,7 @@
     poly_eq_iff ~> poly_eq_poly_eq_iff
     poly_ext ~> poly_eqI
     expand_poly_eq ~> poly_eq_iff
-IMCOMPATIBILTIY.
+IMCOMPATIBILITY.
 
 * Reification and reflection:
   - Reification is now directly available in HOL-Main in structure