--- a/CONTRIBUTORS Tue Jul 01 14:05:05 2014 +0200
+++ b/CONTRIBUTORS Tue Jul 01 14:52:08 2014 +0200
@@ -3,40 +3,48 @@
who is listed as an author in one of the source files of this Isabelle
distribution.
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2014
+-----------------------------
* June 2014: Florian Haftmann, TUM
- Consolidation and generalization of facts concerning products (resp. sums)
- on finite sets.
+ Consolidation and generalization of facts concerning products
+ (resp. sums) on finite sets.
* June 2014: Florian Haftmann, TUM
Internal reorganisation of the local theory / named target stack.
* Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM
- Work on exotic automatic theorem provers for Sledgehammer (LEO-II, veriT,
- Waldmeister, etc.).
+ Work on exotic automatic theorem provers for Sledgehammer (LEO-II,
+ veriT, Waldmeister, etc.).
* June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM
- Various properties of exponentially, Erlang, and normal distributed random variables.
+ Various properties of exponentially, Erlang, and normal distributed
+ random variables.
-* May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM
+* May 2014: Cezary Kaliszyk, University of Innsbruck, and
+ Jasmin Blanchette, TUM
SML-based engines for MaSh.
* March 2014: René Thiemann
Improved code generation for multisets.
* February 2014: Florian Haftmann, TUM
- Permanent interpretation inside theory, locale and class targets with mixin definitions.
+ Permanent interpretation inside theory, locale and class targets
+ with mixin definitions.
+
+* Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI
+ Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
-* Fall 2013 and Winter 2014: Martin Desharnais, 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.
+* Fall 2013 and Winter 2014: Martin Desharnais, 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/Spring 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM
- "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and Z3 4.3.
+* Winter/Spring 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