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