# HG changeset patch
# User blanchet
# Date 1379546126 -7200
# Node ID 2a25bcd8bf78f4d604cbd6bed53ad0869f98f2eb
# Parent  1d88a7ee4e3eb508aad2dd888d2e3f8116984c1a
updated NEWS and CONTRIBUTORS

diff -r 1d88a7ee4e3e -r 2a25bcd8bf78 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Sep 19 01:09:25 2013 +0200
+++ b/CONTRIBUTORS	Thu Sep 19 01:15:26 2013 +0200
@@ -18,6 +18,13 @@
   Various improvements to BNF-based (co)datatype package, including a
   "primrec_new" command and a compatibility layer.
 
+* Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen
+  Jasmin Blanchette, TUM
+  Various improvements to MaSh, including a server mode.
+
+* First half of 2013: Steffen Smolka, TUM
+  Further improvements to Sledgehammer's Isar proof generator.
+
 * Summer 2013: Christian Sternagel, JAIST
   Improved support for ad hoc overloading of constants, including
   documentation and examples.
diff -r 1d88a7ee4e3e -r 2a25bcd8bf78 NEWS
--- a/NEWS	Thu Sep 19 01:09:25 2013 +0200
+++ b/NEWS	Thu Sep 19 01:15:26 2013 +0200
@@ -183,17 +183,20 @@
   for examples.
 
 * HOL/BNF:
-  - Various improvements to BNF-based (co)datatype package, including a
-    "primrec_new" command, a "datatype_new_compat" command, and
+  - Various improvements to BNF-based (co)datatype package, including new
+    commands "primrec_new", "primcorec", and "datatype_new_compat", and
     documentation. See "datatypes.pdf" for details.
   - Renamed keywords:
     data ~> datatype_new
     codata ~> codatatype
     bnf_def ~> bnf
   - Renamed many generated theorems, including
+    discs ~> disc
     map_comp' ~> map_comp
     map_id' ~> map_id
+    sels ~> sel
     set_map' ~> set_map
+    sets ~> set
 IMCOMPATIBILITY.
 
 * Function package: For mutually recursive functions f and g, separate
@@ -386,9 +389,9 @@
 INCOMPATIBILITY.
 
 * Sledgehammer:
-
   - Renamed option:
       isar_shrink ~> isar_compress
+  - Better support for "isar_proofs"
 
 * Imperative-HOL: The MREC combinator is considered legacy and no
 longer included by default. INCOMPATIBILITY, use partial_function