kleing@23382: For the purposes of the license agreement in the file COPYRIGHT, a kleing@23382: '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@20340: wenzelm@23252: Contributions to Isabelle 2007 wenzelm@23252: ------------------------------ wenzelm@23252: wenzelm@23252: * June 2007: Amine Chaieb, TUM wenzelm@23252: Semiring normalization and Groebner Bases wenzelm@17866: paulson@23449: * June 2007: Joe Hurd, Oxford paulson@23449: Metis theorem-prover paulson@23449: paulson@23449: * 2006/2007: Kong W. Susanto, Cambridge paulson@23449: HOL: Metis prover integration. paulson@23449: haftmann@22449: * 2006/2007: Florian Haftmann, TUM haftmann@22449: Pure: generic code generator framework. haftmann@22449: Pure: class package. haftmann@22449: HOL: theory tuning, code generator setup. haftmann@22449: wenzelm@21242: * November 2006: Lukas Bulwahn, TUM wenzelm@21242: HOL/function: method "lexicographic_order". 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@17532: Contributions to Isabelle 2005 wenzelm@17532: ------------------------------ 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$