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@41651: Contributions to this Isabelle version wenzelm@41651: -------------------------------------- wenzelm@41651: wenzelm@41651: wenzelm@41512: Contributions to Isabelle2011 wenzelm@41512: ----------------------------- wenzelm@37383: berghofe@41567: * January 2011: Stefan Berghofer, secunet Security Networks AG berghofe@41567: HOL-SPARK: an interactive prover back-end for SPARK. berghofe@41567: wenzelm@40379: * October 2010: Bogdan Grechuk, University of Edinburgh wenzelm@40379: Extended convex analysis in Multivariate Analysis. wenzelm@40379: wenzelm@40287: * October 2010: Dmitriy Traytel, TUM wenzelm@40287: Coercive subtyping via subtype constraints. wenzelm@40287: krauss@41531: * October 2010: Alexander Krauss, TUM krauss@41531: Command partial_function for function definitions based on complete krauss@41531: partial orders in HOL. krauss@41531: haftmann@39644: * September 2010: Florian Haftmann, TUM wenzelm@41596: Refined concepts for evaluation, i.e., normalization of terms using krauss@41531: different techniques. haftmann@40120: haftmann@40120: * September 2010: Florian Haftmann, TUM haftmann@39644: Code generation for Scala. haftmann@39644: hoelzl@38656: * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM wenzelm@41596: Improved Probability theory in HOL. hoelzl@38656: haftmann@38461: * July 2010: Florian Haftmann, TUM haftmann@39644: Reworking and extension of the Imperative HOL framework. haftmann@38461: wenzelm@41596: * July 2010: Alexander Krauss, TUM and Christian Sternagel, University wenzelm@41596: of Innsbruck krauss@41531: Ad-hoc overloading. Generic do notation for monads. krauss@41531: wenzelm@37383: wenzelm@37144: Contributions to Isabelle2009-2 wenzelm@41512: ------------------------------- wenzelm@33951: krauss@37303: * 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM, krauss@37303: Makarius Wenzel, TUM / LRI krauss@37303: Elimination of type classes from proof terms. krauss@37303: wenzelm@37144: * April 2010: Florian Haftmann, TUM haftmann@36416: Reorganization of abstract algebra type classes. haftmann@36416: wenzelm@37144: * April 2010: Florian Haftmann, TUM haftmann@36416: Code generation for data representations involving invariants; haftmann@36416: various collections avaiable in theories Fset, Dlist, RBT, haftmann@36416: Mapping and AssocList. haftmann@36416: wenzelm@37144: * March 2010: Sascha Boehme, TUM wenzelm@37144: Efficient SHA1 library for Poly/ML. wenzelm@37144: wenzelm@37282: * February 2010: Cezary Kaliszyk and Christian Urban, TUM wenzelm@37282: Quotient type package for Isabelle/HOL. wenzelm@37282: wenzelm@26874: wenzelm@33842: Contributions to Isabelle2009-1 wenzelm@33842: ------------------------------- bulwahn@33649: haftmann@33862: * November 2009, Brian Huffman, PSU haftmann@33862: New definitional domain package for HOLCF. haftmann@33862: hoelzl@33759: * November 2009: Robert Himmelmann, TUM haftmann@33862: Derivation and Brouwer's fixpoint theorem in Multivariate Analysis. hoelzl@33759: wenzelm@33842: * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM wenzelm@33842: A tabled implementation of the reflexive transitive closure. bulwahn@33649: bulwahn@33627: * November 2009: Lukas Bulwahn, TUM wenzelm@33842: Predicate Compiler: a compiler for inductive predicates to wenzelm@33843: equational specifications. bulwahn@33627: wenzelm@33897: * November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris wenzelm@33842: HOL-Boogie: an interactive prover back-end for Boogie and VCC. boehmes@33419: blanchet@33192: * October 2009: Jasmin Blanchette, TUM wenzelm@33842: Nitpick: yet another counterexample generator for Isabelle/HOL. blanchet@33192: boehmes@33010: * October 2009: Sascha Boehme, TUM wenzelm@33182: Extension of SMT method: proof-reconstruction for the SMT solver Z3. boehmes@33010: boehmes@33010: * October 2009: Florian Haftmann, TUM wenzelm@33182: Refinement of parts of the HOL datatype package. haftmann@33005: boehmes@33010: * October 2009: Florian Haftmann, TUM wenzelm@33182: Generic term styles for term antiquotations. haftmann@33005: wenzelm@32762: * September 2009: Thomas Sewell, NICTA wenzelm@33182: More efficient HOL/record implementation. wenzelm@32762: boehmes@32618: * September 2009: Sascha Boehme, TUM wenzelm@33182: SMT method using external SMT solvers. boehmes@32618: haftmann@32600: * September 2009: Florian Haftmann, TUM wenzelm@33182: Refinement of sets and lattices. haftmann@32600: haftmann@32600: * July 2009: Jeremy Avigad and Amine Chaieb wenzelm@33182: New number theory. haftmann@32600: Philipp@32268: * July 2009: Philipp Meyer, TUM wenzelm@33182: HOL/Library/Sum_Of_Squares: functionality to call a remote csdp wenzelm@33182: prover. Philipp@32268: haftmann@31997: * July 2009: Florian Haftmann, TUM wenzelm@33182: New quickcheck implementation using new code generator. haftmann@31997: haftmann@31997: * July 2009: Florian Haftmann, TUM haftmann@39644: HOL/Library/Fset: an explicit type of sets; finite sets ready to use wenzelm@33182: for code generation. haftmann@31466: haftmann@31466: * June 2009: Florian Haftmann, TUM wenzelm@33843: HOL/Library/Tree: search trees implementing mappings, ready to use wenzelm@33182: for code generation. wenzelm@30978: Philipp@32268: * March 2009: Philipp Meyer, TUM wenzelm@33843: Minimization tool for results from Sledgehammer. wenzelm@33182: Philipp@32268: wenzelm@30978: Contributions to Isabelle2009 wenzelm@30978: ----------------------------- wenzelm@30978: wenzelm@30383: * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of wenzelm@30383: Cambridge wenzelm@30383: Elementary topology in Euclidean space. wenzelm@30383: wenzelm@30886: * March 2009: Johannes Hoelzl, TUM wenzelm@30886: Method "approximation", which proves real valued inequalities by wenzelm@30886: computation. wenzelm@30886: wenzelm@30179: * February 2009: Filip Maric, Univ. of Belgrade wenzelm@30179: A Serbian theory. wenzelm@30179: wenzelm@30162: * February 2009: Jasmin Christian Blanchette, TUM wenzelm@30154: Misc cleanup of HOL/refute. wenzelm@30154: wenzelm@30162: * February 2009: Timothy Bourke, NICTA kleing@29883: New find_consts command. kleing@29883: wenzelm@30162: * February 2009: Timothy Bourke, NICTA kleing@29861: "solves" criterion for find_theorems and auto_solve option kleing@29861: haftmann@29398: * December 2008: Clemens Ballarin, TUM haftmann@29398: New locale implementation. haftmann@29398: krauss@29182: * December 2008: Armin Heller, TUM and Alexander Krauss, TUM krauss@29182: Method "sizechange" for advanced termination proofs. krauss@29182: kleing@28901: * November 2008: Timothy Bourke, NICTA kleing@28901: Performance improvement (factor 50) for find_theorems. kleing@28901: haftmann@29398: * 2008: Florian Haftmann, TUM haftmann@29398: Various extensions and restructurings in HOL, improvements haftmann@29398: in evaluation mechanisms, new module binding.ML for name bindings. haftmann@29398: 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@30162: * September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen wenzelm@30162: Prover for coherent logic. wenzelm@30162: 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@30179: 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.