--- 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