CONTRIBUTORS
changeset 57452 ecad2a53755a
parent 57419 2b8b1a8587da
child 57474 250decee4ac5
     1.1 --- a/CONTRIBUTORS	Tue Jul 01 14:05:05 2014 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Jul 01 14:52:08 2014 +0200
     1.3 @@ -3,40 +3,48 @@
     1.4  who is listed as an author in one of the source files of this Isabelle
     1.5  distribution.
     1.6  
     1.7 -Contributions to this Isabelle version
     1.8 ---------------------------------------
     1.9 +Contributions to Isabelle2014
    1.10 +-----------------------------
    1.11  
    1.12  * June 2014: Florian Haftmann, TUM
    1.13 -  Consolidation and generalization of facts concerning products (resp. sums)
    1.14 -  on finite sets.
    1.15 +  Consolidation and generalization of facts concerning products
    1.16 +  (resp. sums) on finite sets.
    1.17  
    1.18  * June 2014: Florian Haftmann, TUM
    1.19    Internal reorganisation of the local theory / named target stack.
    1.20  
    1.21  * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM
    1.22 -  Work on exotic automatic theorem provers for Sledgehammer (LEO-II, veriT,
    1.23 -  Waldmeister, etc.).
    1.24 +  Work on exotic automatic theorem provers for Sledgehammer (LEO-II,
    1.25 +  veriT, Waldmeister, etc.).
    1.26  
    1.27  * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM
    1.28 -  Various properties of exponentially, Erlang, and normal distributed random variables.
    1.29 +  Various properties of exponentially, Erlang, and normal distributed
    1.30 +  random variables.
    1.31  
    1.32 -* May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM
    1.33 +* May 2014: Cezary Kaliszyk, University of Innsbruck, and
    1.34 +  Jasmin Blanchette, TUM
    1.35    SML-based engines for MaSh.
    1.36  
    1.37  * March 2014: René Thiemann
    1.38    Improved code generation for multisets.
    1.39  
    1.40  * February 2014: Florian Haftmann, TUM
    1.41 -  Permanent interpretation inside theory, locale and class targets with mixin definitions.
    1.42 +  Permanent interpretation inside theory, locale and class targets
    1.43 +  with mixin definitions.
    1.44 +
    1.45 +* Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI
    1.46 +  Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
    1.47  
    1.48 -* Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, Dmitriy Traytel,
    1.49 -  and Jasmin Blanchette, TUM
    1.50 -  Various improvements to the BNF-based (co)datatype package, including
    1.51 -  a more polished "primcorec" command, optimizations, and integration in
    1.52 -  the "HOL" session.
    1.53 +* Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny,
    1.54 +  Dmitriy Traytel, and Jasmin Blanchette, TUM
    1.55 +  Various improvements to the BNF-based (co)datatype package,
    1.56 +  including a more polished "primcorec" command, optimizations, and
    1.57 +  integration in the "HOL" session.
    1.58  
    1.59 -* Winter/Spring 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM
    1.60 -  "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and Z3 4.3.
    1.61 +* Winter/Spring 2014: Sascha Boehme, QAware GmbH, and
    1.62 +  Jasmin Blanchette, TUM
    1.63 +  "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and
    1.64 +  Z3 4.3.
    1.65  
    1.66  * January 2014: Lars Hupel, TUM
    1.67    An improved, interactive simplifier trace with integration into the