CONTRIBUTORS
changeset 56118 d3967fdc800a
parent 55913 c1409c103b77
child 56416 b9baecff0684
--- a/CONTRIBUTORS	Thu Mar 13 16:07:27 2014 -0700
+++ b/CONTRIBUTORS	Fri Mar 14 01:28:13 2014 +0100
@@ -9,6 +9,15 @@
 * March 2014: René Thiemann
   Improved code generation for multisets.
 
+* Fall 2013 and Winter 2014: Lorenz Panny, Dmitriy Traytel, and
+  Jasmin Blanchette, TUM
+  Various improvements to the BNF-based (co)datatype package, including
+  a more polished "primcorec" command, optimizations, and integration in
+  the "HOL" session.
+
+* Winter 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM
+  "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and Z3 4.3.
+
 * January 2014: Lars Hupel, TUM
   An improved, interactive simplifier trace with integration into the
   Isabelle/jEdit Prover IDE.
@@ -42,7 +51,7 @@
 
 * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and
   Jasmin Blanchette, TUM
-  Various improvements to BNF-based (co)datatype package, including
+  Various improvements to the BNF-based (co)datatype package, including
   "primrec_new" and "primcorec" commands and a compatibility layer.
 
 * Spring and Summer 2013: Ondrej Kuncar, TUM