updated NEWS and CONTRIBUTORS
authorblanchet
Thu, 19 Sep 2013 01:15:26 +0200
changeset 53728 2a25bcd8bf78
parent 53727 1d88a7ee4e3e
child 53729 b9d727a767ea
updated NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
--- 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.
--- 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