wenzelm@24799: For the purposes of the license agreement in the file COPYRIGHT, a wenzelm@24799: 'contributor' is anybody who is listed in this file (CONTRIBUTORS) or kleing@23382: who is listed as an author in one of the source files of this Isabelle kleing@23382: distribution. kleing@23382: wenzelm@26874: wenzelm@25468: Contributions to this Isabelle version wenzelm@25468: -------------------------------------- wenzelm@25468: kleing@28901: * November 2008: Timothy Bourke, NICTA kleing@28901: Performance improvement (factor 50) for find_theorems. kleing@28901: wenzelm@28604: * October 2008: Fabian Immler, TUM wenzelm@28604: ATP manager for Sledgehammer, based on ML threads instead of Posix wenzelm@28604: processes. Additional ATP wrappers, including remote SystemOnTPTP wenzelm@28604: services. wenzelm@28604: wenzelm@28474: * August 2008: Fabian Immler, TUM wenzelm@28474: Vampire wrapper script for remote SystemOnTPTP service. wenzelm@28474: wenzelm@28474: wenzelm@28474: Contributions to Isabelle2008 wenzelm@28474: ----------------------------- wenzelm@28474: wenzelm@27009: * 2007/2008: wenzelm@27009: Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM wenzelm@27009: HOL library improvements. wenzelm@25468: wenzelm@27009: * 2007/2008: Brian Huffman, PSU wenzelm@27009: HOLCF library improvements. wenzelm@27009: wenzelm@27009: * 2007/2008: Stefan Berghofer, TUM wenzelm@27009: HOL-Nominal package improvements. wenzelm@27009: wenzelm@27009: * March 2008: Markus Reiter, TUM wenzelm@27009: HOL/Library/RBT: red-black trees. haftmann@26728: wenzelm@26874: * February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and wenzelm@26874: Lukas Bulwahn, TUM and John Matthews, Galois: wenzelm@26874: HOL/Library/Imperative_HOL: Haskell-style imperative data structures wenzelm@26874: for HOL. haftmann@26728: wenzelm@27009: * December 2007: Norbert Schirmer, Uni Saarbruecken wenzelm@27009: Misc improvements of record package in HOL. wenzelm@27009: wenzelm@27009: * December 2007: Florian Haftmann, TUM wenzelm@27009: Overloading and class instantiation target. wenzelm@27009: wenzelm@27009: * December 2007: Florian Haftmann, TUM wenzelm@27009: New version of primrec package for local theories. wenzelm@27009: wenzelm@27009: * December 2007: Alexander Krauss, TUM wenzelm@27009: Method "induction_scheme" in HOL. wenzelm@27009: wenzelm@27009: * November 2007: Peter Lammich, Uni Muenster wenzelm@27009: HOL-Lattice: some more lemmas. wenzelm@26198: wenzelm@26874: wenzelm@25454: Contributions to Isabelle2007 wenzelm@25454: ----------------------------- wenzelm@23252: schirmer@25409: * October 2007: Norbert Schirmer, TUM / Uni Saarbruecken wenzelm@25398: State Spaces: The Locale Way (in HOL). wenzelm@25398: wenzelm@25057: * October 2007: Mark A. Hillebrand, DFKI wenzelm@25057: Robust sub/superscripts in LaTeX document output. wenzelm@25057: wenzelm@24799: * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian wenzelm@24799: Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois kleing@24333: HOL-Word: a library for fixed-size machine words in Isabelle. kleing@24333: kleing@24332: * August 2007: Brian Huffman, PSU wenzelm@24799: HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type. kleing@24332: wenzelm@23252: * June 2007: Amine Chaieb, TUM wenzelm@24799: Semiring normalization and Groebner Bases. wenzelm@25449: Support for dense linear orders. wenzelm@17866: paulson@23449: * June 2007: Joe Hurd, Oxford wenzelm@24799: Metis theorem-prover. wenzelm@24799: wenzelm@24799: * 2007: Kong W. Susanto, Cambridge wenzelm@24799: HOL: Metis prover integration. paulson@23449: wenzelm@24799: * 2007: Stefan Berghofer, TUM wenzelm@25449: HOL: inductive predicates and sets. wenzelm@24799: wenzelm@24803: * 2007: Norbert Schirmer, TUM wenzelm@24803: HOL/record: misc improvements. wenzelm@24803: wenzelm@24799: * 2006/2007: Alexander Krauss, TUM wenzelm@24799: HOL: function package and related theories on termination. paulson@23449: haftmann@22449: * 2006/2007: Florian Haftmann, TUM haftmann@22449: Pure: generic code generator framework. haftmann@22449: Pure: class package. wenzelm@24799: HOL: theory reorganization, code generator setup. wenzelm@24799: wenzelm@25449: * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and wenzelm@25449: Julien Narboux, TUM wenzelm@24799: HOL/Nominal package and related tools. haftmann@22449: wenzelm@21242: * November 2006: Lukas Bulwahn, TUM wenzelm@24799: HOL: method "lexicographic_order" for function package. wenzelm@21242: wenzelm@21169: * October 2006: Stefan Hohe, TUM wenzelm@21169: HOL-Algebra: ideals and quotients over rings. wenzelm@21169: wenzelm@20340: * August 2006: Amine Chaieb, TUM wenzelm@20340: Experimental support for generic reflection and reification in HOL. wenzelm@20340: kleing@20067: * July 2006: Rafal Kolanski, NICTA kleing@20067: Hex (0xFF) and binary (0b1011) numerals. kleing@20067: nipkow@19896: * May 2006: Klaus Aehlig, LMU nipkow@19896: Command 'normal_form': normalization by evaluation. nipkow@19896: wenzelm@19650: * May 2006: Amine Chaieb, TUM wenzelm@19650: HOL-Complex: Ferrante and Rackoff Algorithm for linear real wenzelm@19650: arithmetic. kleing@19470: kleing@19470: * February 2006: Benjamin Porter, NICTA kleing@23382: HOL and HOL-Complex: generalised mean value theorem, continuum is kleing@19470: not denumerable, harmonic and arithmetic series, and denumerability kleing@19470: of rationals. wenzelm@17532: wenzelm@19650: * October 2005: Martin Wildmoser, TUM wenzelm@19650: Sketch for Isar 'guess' element. wenzelm@19650: wenzelm@19650: wenzelm@25454: Contributions to Isabelle2005 wenzelm@25454: ----------------------------- wenzelm@17382: wenzelm@17640: * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM wenzelm@17640: HOL-Complex: Formalization of Taylor series. wenzelm@17640: wenzelm@17640: * September 2005: Stephan Merz, Alwen Tiu, QSL Loria wenzelm@17640: Components for SAT solver method using zChaff. wenzelm@17640: wenzelm@17534: * September 2005: Ning Zhang and Christian Urban, LMU Munich wenzelm@17534: A Chinese theory. wenzelm@17534: wenzelm@17562: * September 2005: Bernhard Haeupler, TUM wenzelm@17382: Method comm_ring for proving equalities in commutative rings. wenzelm@16892: wenzelm@17532: * July/August 2005: Jeremy Avigad, Carnegie Mellon University wenzelm@16892: Various improvements of the HOL and HOL-Complex library. wenzelm@16868: wenzelm@16892: * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM wenzelm@16892: Some structured proofs about completeness of real numbers. wenzelm@16892: wenzelm@17532: * May 2005: Rafal Kolanski and Gerwin Klein, NICTA wenzelm@17532: Improved retrieval of facts from theory/proof context. wenzelm@15994: wenzelm@16252: * February 2005: Lucas Dixon, University of Edinburgh wenzelm@17532: Improved subst method. wenzelm@17532: wenzelm@17532: * 2005: Brian Huffman, OGI wenzelm@17532: Various improvements of HOLCF. wenzelm@17532: Some improvements of the HOL-Complex library. wenzelm@17532: wenzelm@17532: * 2005: Claire Quigley and Jia Meng, University of Cambridge wenzelm@17532: Some support for asynchronous communication with external provers wenzelm@17532: (experimental). wenzelm@17532: wenzelm@17532: * 2005: Florian Haftmann, TUM wenzelm@17543: Contributions to document 'sugar'. wenzelm@17532: Various ML combinators, notably linear functional transformations. wenzelm@17532: Some cleanup of ML legacy. wenzelm@17532: Additional antiquotations. wenzelm@17532: Improved Isabelle web site. wenzelm@17532: wenzelm@17532: * 2004/2005: David Aspinall, University of Edinburgh wenzelm@17532: Various elements of XML and PGIP based communication with user wenzelm@17532: interfaces (experimental). wenzelm@17532: wenzelm@17532: * 2004/2005: Gerwin Klein, NICTA wenzelm@17532: Contributions to document 'sugar'. wenzelm@17532: Improved Isabelle web site. wenzelm@17532: Improved HTML presentation of theories. wenzelm@17532: wenzelm@17532: * 2004/2005: Clemens Ballarin, TUM wenzelm@17532: Provers: tools for transitive relations and quasi orders. wenzelm@17532: Improved version of locales, notably interpretation of locales. wenzelm@17532: Improved version of HOL-Algebra. wenzelm@17532: wenzelm@17532: * 2004/2005: Amine Chaieb, TUM wenzelm@17532: Improved version of HOL presburger method. wenzelm@17532: wenzelm@17532: * 2004/2005: Steven Obua, TUM wenzelm@17532: Improved version of HOL/Import, support for HOL-Light. wenzelm@17532: Improved version of HOL-Complex-Matrix. wenzelm@17572: Pure/defs: more sophisticated checks on well-formedness of overloading. wenzelm@17543: Pure/Tools: an experimental evaluator for lambda terms. wenzelm@17532: wenzelm@17532: * 2004/2005: Norbert Schirmer, TUM wenzelm@17532: Contributions to document 'sugar'. wenzelm@17532: Improved version of HOL/record. wenzelm@17532: wenzelm@17532: * 2004/2005: Sebastian Skalberg, TUM wenzelm@17532: Improved version of HOL/Import. wenzelm@17532: Some internal ML reorganizations. wenzelm@17532: wenzelm@17532: * 2004/2005: Tjark Weber, TUM wenzelm@17640: SAT solver method using zChaff. wenzelm@17532: Improved version of HOL/refute. wenzelm@16252: wenzelm@15994: $Id$