1.1 --- a/CONTRIBUTORS	Thu Sep 19 01:09:25 2013 +0200
     1.2 +++ b/CONTRIBUTORS	Thu Sep 19 01:15:26 2013 +0200
     1.3 @@ -18,6 +18,13 @@
     1.4    Various improvements to BNF-based (co)datatype package, including a
     1.5    "primrec_new" command and a compatibility layer.
     1.6  
     1.7 +* Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen
     1.8 +  Jasmin Blanchette, TUM
     1.9 +  Various improvements to MaSh, including a server mode.
    1.10 +
    1.11 +* First half of 2013: Steffen Smolka, TUM
    1.12 +  Further improvements to Sledgehammer's Isar proof generator.
    1.13 +
    1.14  * Summer 2013: Christian Sternagel, JAIST
    1.15    Improved support for ad hoc overloading of constants, including
    1.16    documentation and examples.

     2.1 --- a/NEWS	Thu Sep 19 01:09:25 2013 +0200
     2.2 +++ b/NEWS	Thu Sep 19 01:15:26 2013 +0200
     2.3 @@ -183,17 +183,20 @@
     2.4    for examples.
     2.5  
     2.6  * HOL/BNF:
     2.7 -  - Various improvements to BNF-based (co)datatype package, including a
     2.8 -    "primrec_new" command, a "datatype_new_compat" command, and
     2.9 +  - Various improvements to BNF-based (co)datatype package, including new
    2.10 +    commands "primrec_new", "primcorec", and "datatype_new_compat", and
    2.11      documentation. See "datatypes.pdf" for details.
    2.12    - Renamed keywords:
    2.13      data ~> datatype_new
    2.14      codata ~> codatatype
    2.15      bnf_def ~> bnf
    2.16    - Renamed many generated theorems, including
    2.17 +    discs ~> disc
    2.18      map_comp' ~> map_comp
    2.19      map_id' ~> map_id
    2.20 +    sels ~> sel
    2.21      set_map' ~> set_map
    2.22 +    sets ~> set
    2.23  IMCOMPATIBILITY.
    2.24  
    2.25  * Function package: For mutually recursive functions f and g, separate
    2.26 @@ -386,9 +389,9 @@
    2.27  INCOMPATIBILITY.
    2.28  
    2.29  * Sledgehammer:
    2.30 -
    2.31    - Renamed option:
    2.32        isar_shrink ~> isar_compress
    2.33 +  - Better support for "isar_proofs"
    2.34  
    2.35  * Imperative-HOL: The MREC combinator is considered legacy and no
    2.36  longer included by default. INCOMPATIBILITY, use partial_function