CONTRIBUTORS
author wenzelm
Mon Oct 01 21:19:50 2007 +0200 (2007-10-01)
changeset 24803 38577b4b1fde
parent 24799 dff164b6f2a6
child 25057 021fcbe2aaa5
permissions -rw-r--r--
Norbert Schirmer: record improvements;
     1 For the purposes of the license agreement in the file COPYRIGHT, a
     2 'contributor' is anybody who is listed in this file (CONTRIBUTORS) or
     3 who is listed as an author in one of the source files of this Isabelle
     4 distribution.
     5 
     6 
     7 Contributions to Isabelle 2007
     8 ------------------------------
     9 
    10 * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian
    11     Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois
    12   HOL-Word: a library for fixed-size machine words in Isabelle.
    13 
    14 * August 2007: Brian Huffman, PSU
    15   HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type.
    16 
    17 * June 2007: Amine Chaieb, TUM
    18   Semiring normalization and Groebner Bases.
    19   Support for dens linear orders.
    20 
    21 * June 2007: Joe Hurd, Oxford
    22   Metis theorem-prover.
    23 
    24 * 2007: Kong W. Susanto, Cambridge
    25   HOL: Metis prover integration.
    26 
    27 * 2007: Stefan Berghofer, TUM
    28   HOL: inductive predicates.
    29 
    30 * 2007: Norbert Schirmer, TUM
    31   HOL/record: misc improvements.
    32 
    33 * 2006/2007: Alexander Krauss, TUM
    34   HOL: function package and related theories on termination.
    35 
    36 * 2006/2007: Florian Haftmann, TUM
    37   Pure: generic code generator framework.
    38   Pure: class package.
    39   HOL: theory reorganization, code generator setup.
    40 
    41 * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and Julien
    42   Narboux, TUM
    43   HOL/Nominal package and related tools.
    44 
    45 * November 2006: Lukas Bulwahn, TUM
    46   HOL: method "lexicographic_order" for function package.
    47 
    48 * October 2006: Stefan Hohe, TUM
    49   HOL-Algebra: ideals and quotients over rings.
    50 
    51 * August 2006: Amine Chaieb, TUM
    52   Experimental support for generic reflection and reification in HOL.
    53 
    54 * July 2006: Rafal Kolanski, NICTA
    55   Hex (0xFF) and binary (0b1011) numerals.
    56 
    57 * May 2006: Klaus Aehlig, LMU
    58   Command 'normal_form': normalization by evaluation.
    59 
    60 * May 2006: Amine Chaieb, TUM
    61   HOL-Complex: Ferrante and Rackoff Algorithm for linear real
    62   arithmetic.
    63 
    64 * February 2006: Benjamin Porter, NICTA
    65   HOL and HOL-Complex: generalised mean value theorem, continuum is
    66   not denumerable, harmonic and arithmetic series, and denumerability
    67   of rationals.
    68 
    69 * October 2005: Martin Wildmoser, TUM
    70   Sketch for Isar 'guess' element.
    71 
    72 
    73 Contributions to Isabelle 2005
    74 ------------------------------
    75 
    76 * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
    77   HOL-Complex: Formalization of Taylor series.
    78 
    79 * September 2005: Stephan Merz, Alwen Tiu, QSL Loria
    80   Components for SAT solver method using zChaff.
    81 
    82 * September 2005: Ning Zhang and Christian Urban, LMU Munich
    83   A Chinese theory.
    84 
    85 * September 2005: Bernhard Haeupler, TUM
    86   Method comm_ring for proving equalities in commutative rings.
    87 
    88 * July/August 2005: Jeremy Avigad, Carnegie Mellon University
    89   Various improvements of the HOL and HOL-Complex library.
    90 
    91 * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
    92   Some structured proofs about completeness of real numbers.
    93 
    94 * May 2005: Rafal Kolanski and Gerwin Klein, NICTA
    95   Improved retrieval of facts from theory/proof context.
    96 
    97 * February 2005: Lucas Dixon, University of Edinburgh
    98   Improved subst method.
    99 
   100 * 2005: Brian Huffman, OGI
   101   Various improvements of HOLCF.
   102   Some improvements of the HOL-Complex library.
   103 
   104 * 2005: Claire Quigley and Jia Meng, University of Cambridge
   105   Some support for asynchronous communication with external provers
   106   (experimental).
   107 
   108 * 2005: Florian Haftmann, TUM
   109   Contributions to document 'sugar'.
   110   Various ML combinators, notably linear functional transformations.
   111   Some cleanup of ML legacy.
   112   Additional antiquotations.
   113   Improved Isabelle web site.
   114 
   115 * 2004/2005: David Aspinall, University of Edinburgh
   116   Various elements of XML and PGIP based communication with user
   117   interfaces (experimental).
   118 
   119 * 2004/2005: Gerwin Klein, NICTA
   120   Contributions to document 'sugar'.
   121   Improved Isabelle web site.
   122   Improved HTML presentation of theories.
   123 
   124 * 2004/2005: Clemens Ballarin, TUM
   125   Provers: tools for transitive relations and quasi orders.
   126   Improved version of locales, notably interpretation of locales.
   127   Improved version of HOL-Algebra.
   128 
   129 * 2004/2005: Amine Chaieb, TUM
   130   Improved version of HOL presburger method.
   131 
   132 * 2004/2005: Steven Obua, TUM
   133   Improved version of HOL/Import, support for HOL-Light.
   134   Improved version of HOL-Complex-Matrix.
   135   Pure/defs: more sophisticated checks on well-formedness of overloading.
   136   Pure/Tools: an experimental evaluator for lambda terms.
   137 
   138 * 2004/2005: Norbert Schirmer, TUM
   139   Contributions to document 'sugar'.
   140   Improved version of HOL/record.
   141 
   142 * 2004/2005: Sebastian Skalberg, TUM
   143   Improved version of HOL/Import.
   144   Some internal ML reorganizations.
   145 
   146 * 2004/2005: Tjark Weber, TUM
   147   SAT solver method using zChaff.
   148   Improved version of HOL/refute.
   149 
   150 $Id$