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