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