more contributions;
authorwenzelm
Tue Sep 20 21:48:37 2005 +0200 (2005-09-20)
changeset 17532ab75f2b0cec6
parent 17531 0bc8ae586a7c
child 17533 f22f2ffd78ba
more contributions;
CONTRIBUTORS
     1.1 --- a/CONTRIBUTORS	Tue Sep 20 21:39:00 2005 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Sep 20 21:48:37 2005 +0200
     1.3 @@ -1,24 +1,67 @@
     1.4 +
     1.5 +Contributions to Isabelle 2005
     1.6 +------------------------------
     1.7  
     1.8  * September 2005: Bernhard Haeupler
     1.9    Method comm_ring for proving equalities in commutative rings.
    1.10  
    1.11 -* July 2005: Jeremy Avigad, Carnegie Mellon University
    1.12 +* July/August 2005: Jeremy Avigad, Carnegie Mellon University
    1.13    Various improvements of the HOL and HOL-Complex library.
    1.14  
    1.15 -* July 2005: Florian Haftmann, TUM
    1.16 -  Some combinators for linear functional transformations in ML:
    1.17 -  |->  #->  fold_map  etc.
    1.18 -
    1.19  * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
    1.20    Some structured proofs about completeness of real numbers.
    1.21  
    1.22 -* May 2005: Rafal Kolanski, NICTA
    1.23 -  Substantially improved retrieval of facts from theory/proof context.
    1.24 -
    1.25 -* May 2005: Florian Haftmann, TUM
    1.26 -  Several new antiquotation.
    1.27 +* May 2005: Rafal Kolanski and Gerwin Klein, NICTA
    1.28 +  Improved retrieval of facts from theory/proof context.
    1.29  
    1.30  * February 2005: Lucas Dixon, University of Edinburgh
    1.31 -  Substantially improved subst method.
    1.32 +  Improved subst method.
    1.33 +
    1.34 +* 2005: Brian Huffman, OGI
    1.35 +  Various improvements of HOLCF.
    1.36 +  Some improvements of the HOL-Complex library.
    1.37 +
    1.38 +* 2005: Claire Quigley and Jia Meng, University of Cambridge
    1.39 +  Some support for asynchronous communication with external provers
    1.40 +  (experimental).
    1.41 +
    1.42 +* 2005: Florian Haftmann, TUM
    1.43 +  Various ML combinators, notably linear functional transformations.
    1.44 +  Some cleanup of ML legacy.
    1.45 +  Additional antiquotations.
    1.46 +  Improved Isabelle web site.
    1.47 +
    1.48 +* 2004/2005: David Aspinall, University of Edinburgh
    1.49 +  Various elements of XML and PGIP based communication with user
    1.50 +  interfaces (experimental).
    1.51 +
    1.52 +* 2004/2005: Gerwin Klein, NICTA
    1.53 +  Contributions to document 'sugar'.
    1.54 +  Improved Isabelle web site.
    1.55 +  Improved HTML presentation of theories.
    1.56 +
    1.57 +* 2004/2005: Clemens Ballarin, TUM
    1.58 +  Provers: tools for transitive relations and quasi orders.
    1.59 +  Improved version of locales, notably interpretation of locales.
    1.60 +  Improved version of HOL-Algebra.
    1.61 +
    1.62 +* 2004/2005: Amine Chaieb, TUM
    1.63 +  Improved version of HOL presburger method.
    1.64 +
    1.65 +* 2004/2005: Steven Obua, TUM
    1.66 +  Pure/defs: more sophisticated check on well-formedness of overloading.
    1.67 +  Improved version of HOL/Import, support for HOL-Light.
    1.68 +  Improved version of HOL-Complex-Matrix.
    1.69 +
    1.70 +* 2004/2005: Norbert Schirmer, TUM
    1.71 +  Contributions to document 'sugar'.
    1.72 +  Improved version of HOL/record.
    1.73 +
    1.74 +* 2004/2005: Sebastian Skalberg, TUM
    1.75 +  Improved version of HOL/Import.
    1.76 +  Some internal ML reorganizations.
    1.77 +
    1.78 +* 2004/2005: Tjark Weber, TUM
    1.79 +  Improved version of HOL/refute.
    1.80  
    1.81  $Id$