updated news/contributors with BNF stuff
authorblanchet
Fri Aug 30 12:06:37 2013 +0200 (2013-08-30 ago)
changeset 53307221ff2b39a35
parent 53306 45f13517693a
child 53308 d066e4923a31
updated news/contributors with BNF stuff
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Fri Aug 30 12:06:11 2013 +0200
     1.2 +++ b/CONTRIBUTORS	Fri Aug 30 12:06:37 2013 +0200
     1.3 @@ -6,8 +6,12 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and Jasmin Blanchette, TUM
     1.8 +  Various improvements to BNF-based (co)datatype package, including a
     1.9 +  "primrec_new" command and a compatibility layer.
    1.10 +
    1.11  * Summer 2013: Christian Sternagel, JAIST
    1.12 -  Improved support for adhoc overloading of constants, including
    1.13 +  Improved support for ad hoc overloading of constants, including
    1.14    documentation and examples.
    1.15  
    1.16  * May 2013: Florian Haftmann, TUM
     2.1 --- a/NEWS	Fri Aug 30 12:06:11 2013 +0200
     2.2 +++ b/NEWS	Fri Aug 30 12:06:37 2013 +0200
     2.3 @@ -141,7 +141,7 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 -* Improved support for adhoc overloading of constants (see also
     2.8 +* Improved support for ad hoc overloading of constants (see also
     2.9  isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).
    2.10  
    2.11  * Attibute 'code': 'code' now declares concrete and abstract code
    2.12 @@ -156,6 +156,20 @@
    2.13    See the isar-ref manual for syntax diagrams, and the HOL theories
    2.14    for examples.
    2.15  
    2.16 +* HOL/BNF:
    2.17 +  - Various improvements to BNF-based (co)datatype package, including a
    2.18 +    "primrec_new" command, a "datatype_compat" command, and
    2.19 +    documentation. See "datatypes.pdf" for details.
    2.20 +  - Renamed keywords:
    2.21 +    data ~> datatype_new
    2.22 +    codata ~> codatatype
    2.23 +    bnf_def ~> bnf
    2.24 +  - Renamed many generated theorems, including
    2.25 +    map_comp' ~> map_comp
    2.26 +    map_id' ~> map_id
    2.27 +    set_map' ~> set_map
    2.28 +IMCOMPATIBILITY.
    2.29 +
    2.30  * Library/Polynomial.thy:
    2.31    - Use lifting for primitive definitions.
    2.32    - Explicit conversions from and to lists of coefficients, used for
    2.33 @@ -166,7 +180,7 @@
    2.34      poly_eq_iff ~> poly_eq_poly_eq_iff
    2.35      poly_ext ~> poly_eqI
    2.36      expand_poly_eq ~> poly_eq_iff
    2.37 -IMCOMPATIBILTIY.
    2.38 +IMCOMPATIBILITY.
    2.39  
    2.40  * Reification and reflection:
    2.41    - Reification is now directly available in HOL-Main in structure