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