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@53984: Contributions to Isabelle2013-1 wenzelm@53984: ------------------------------- wenzelm@50994: noschinl@54363: * September 2013: Lars Noschinski, TUM wenzelm@54364: Conversion between function definitions as list of equations and wenzelm@54364: case expressions in HOL. wenzelm@54364: New library Simps_Case_Conv with commands case_of_simps, wenzelm@54364: simps_of_case. noschinl@54363: wenzelm@53396: * September 2013: Nik Sultana, University of Cambridge wenzelm@53396: Improvements to HOL/TPTP parser and import facilities. wenzelm@53396: traytel@54029: * September 2013: Johannes Hölzl and Dmitriy Traytel, TUM traytel@54029: New "coinduction" method (residing in HOL-BNF) to avoid boilerplate. traytel@54029: wenzelm@53984: * Summer 2013: Makarius Wenzel, Université Paris-Sud / LRI wenzelm@53984: Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. wenzelm@53984: krauss@53613: * Summer 2013: Manuel Eberl, TUM krauss@53613: Generation of elimination rules in the function package. krauss@53613: New command "fun_cases". krauss@53613: wenzelm@54051: * Summer 2013: Christian Sternagel, JAIST wenzelm@54051: Improved support for ad hoc overloading of constants, including wenzelm@54051: documentation and examples. wenzelm@54051: wenzelm@53396: * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and wenzelm@53396: Jasmin Blanchette, TUM blanchet@53767: Various improvements to BNF-based (co)datatype package, including blanchet@54010: "primrec_new" and "primcorec" commands and a compatibility layer. blanchet@53307: kuncar@54021: * Spring and Summer 2013: Ondrej Kuncar, TUM wenzelm@54035: Various improvements of Lifting and Transfer packages. kuncar@54021: kuncar@54021: * Spring 2013: Brian Huffman, Galois Inc. wenzelm@54035: Improvements of the Transfer package. wenzelm@54051: blanchet@53728: * Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen blanchet@53728: Jasmin Blanchette, TUM blanchet@53728: Various improvements to MaSh, including a server mode. blanchet@53728: blanchet@53728: * First half of 2013: Steffen Smolka, TUM blanchet@53728: Further improvements to Sledgehammer's Isar proof generator. blanchet@53728: haftmann@52485: * May 2013: Florian Haftmann, TUM haftmann@52485: Ephemeral interpretation in local theories. haftmann@52485: bulwahn@52266: * May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM wenzelm@53164: Spec_Check: A Quickcheck tool for Isabelle/ML. bulwahn@52266: traytel@51682: * April 2013: Stefan Berghofer, secunet Security Networks AG traytel@51682: Dmitriy Traytel, TUM traytel@51682: Makarius Wenzel, Université Paris-Sud / LRI traytel@51682: Case translations as a separate check phase independent of the traytel@51682: datatype package. traytel@51682: haftmann@51487: * March 2013: Florian Haftmann, TUM haftmann@51489: Reform of "big operators" on sets. haftmann@51489: haftmann@51489: * March 2013: Florian Haftmann, TUM haftmann@51487: Algebraic locale hierarchy for orderings and (semi)lattices. haftmann@51487: wenzelm@52503: * February 2013: Florian Haftmann, TUM wenzelm@52503: Reworking and consolidation of code generation for target language wenzelm@52503: numerals. haftmann@51167: wenzelm@52503: * February 2013: Florian Haftmann, TUM haftmann@51173: Sieve of Eratosthenes. haftmann@51173: haftmann@51167: wenzelm@50993: Contributions to Isabelle2013 wenzelm@50993: ----------------------------- wenzelm@47887: wenzelm@49532: * 2012: Makarius Wenzel, Université Paris-Sud / LRI wenzelm@49532: Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. wenzelm@49532: wenzelm@50648: * Fall 2012: Daniel Kühlwein, ICIS, Radboud University Nijmegen blanchet@50222: Jasmin Blanchette, TUM blanchet@50222: Implemented Machine Learning for Sledgehammer (MaSh). blanchet@50222: blanchet@50219: * Fall 2012: Steffen Smolka, TUM wenzelm@50648: Various improvements to Sledgehammer's Isar proof generator, wenzelm@50648: including a smart type annotation algorithm and proof shrinking. blanchet@50219: nipkow@50573: * December 2012: Alessandro Coglio, Kestrel wenzelm@50991: Contributions to HOL's Lattice library. nipkow@50573: hoelzl@50142: * November 2012: Fabian Immler, TUM wenzelm@50184: "Symbols" dockable for Isabelle/jEdit. wenzelm@50184: wenzelm@50184: * November 2012: Fabian Immler, TUM wenzelm@50184: Proof of the Daniell-Kolmogorov theorem: the existence of the limit wenzelm@50184: of projective families. hoelzl@50142: Andreas@49770: * October 2012: Andreas Lochbihler, KIT wenzelm@50184: Efficient construction of red-black trees from sorted associative wenzelm@50184: lists. Andreas@49770: haftmann@49190: * September 2012: Florian Haftmann, TUM haftmann@49190: Lattice instances for type option. haftmann@49190: Christian@49145: * September 2012: Christian Sternagel, JAIST Christian@49145: Consolidated HOL/Library (theories: Prefix_Order, Sublist, and Christian@49145: Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists. Christian@49145: blanchet@48977: * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM blanchet@49510: New BNF-based (co)datatype package. blanchet@48977: blanchet@48977: * August 2012: Andrei Popescu and Dmitriy Traytel, TUM blanchet@48977: Theories of ordinals and cardinals. blanchet@48977: wenzelm@48585: * July 2012: Makarius Wenzel, Université Paris-Sud / LRI wenzelm@48585: Advanced support for Isabelle sessions and build management, notably wenzelm@48585: "isabelle build". wenzelm@48585: bulwahn@48111: * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA wenzelm@48585: Simproc for rewriting set comprehensions into pointfree expressions. wenzelm@47887: Andreas@49481: * May 2012: Andreas Lochbihler, KIT Andreas@49481: Theory of almost everywhere constant functions. wenzelm@48124: wenzelm@50648: * 2010-2012: Markus Kaiser and Lukas Bulwahn, TUM wenzelm@50648: Graphview in Scala/Swing. wenzelm@50648: wenzelm@50648: wenzelm@47462: Contributions to Isabelle2012 wenzelm@47462: ----------------------------- wenzelm@45109: hoelzl@47695: * April 2012: Johannes Hölzl, TUM wenzelm@47808: Probability: Introduced type to represent measures instead of wenzelm@47808: locales. hoelzl@47695: hoelzl@47695: * April 2012: Johannes Hölzl, Fabian Immler, TUM hoelzl@47695: Float: Moved to Dyadic rationals to represent floating point numers. hoelzl@47695: wenzelm@47808: * April 2012: Thomas Sewell, NICTA and wenzelm@47808: 2010: Sascha Boehme, TUM wenzelm@47808: Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector wenzelm@47808: equalities/inequalities. thomas@47567: wenzelm@47808: * March 2012: Christian Sternagel, JAIST bulwahn@47448: Consolidated theory of relation composition. bulwahn@47448: wenzelm@47413: * March 2012: Nik Sultana, University of Cambridge wenzelm@47413: HOL/TPTP parser and import facilities. wenzelm@47413: wenzelm@47462: * March 2012: Cezary Kaliszyk, University of Innsbruck and wenzelm@47462: Alexander Krauss, QAware GmbH wenzelm@47462: Faster and more scalable Import mechanism for HOL Light proofs. wenzelm@47462: blanchet@47563: * January 2012: Florian Haftmann, TUM, et al. haftmann@46596: (Re-)Introduction of the "set" type constructor. haftmann@46596: kuncar@47700: * 2012: Ondrej Kuncar, TUM wenzelm@47808: New package Lifting, various improvements and refinements to the wenzelm@47808: Quotient package. kuncar@47700: blanchet@47563: * 2011/2012: Jasmin Blanchette, TUM blanchet@47563: Various improvements to Sledgehammer, notably: tighter integration wenzelm@47808: with SPASS, support for more provers (Alt-Ergo, iProver, wenzelm@47808: iProver-Eq). blanchet@47563: wenzelm@47462: * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI wenzelm@47485: Various refinements of local theory infrastructure. wenzelm@47462: Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE. krauss@47265: wenzelm@45109: wenzelm@44801: Contributions to Isabelle2011-1 wenzelm@44801: ------------------------------- wenzelm@41651: haftmann@44818: * September 2011: Peter Gammie huffman@44908: Theory HOL/Library/Saturated: numbers with saturated arithmetic. haftmann@44818: haftmann@44818: * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM haftmann@44818: Refined theory on complete lattices. haftmann@44818: wenzelm@44967: * August 2011: Brian Huffman, Portland State University wenzelm@44967: Miscellaneous cleanup of Complex_Main and Multivariate_Analysis. wenzelm@44967: wenzelm@44967: * June 2011: Brian Huffman, Portland State University wenzelm@44967: Proof method "countable_datatype" for theory Library/Countable. wenzelm@44967: wenzelm@44967: * 2011: Jasmin Blanchette, TUM wenzelm@44967: Various improvements to Sledgehammer, notably: use of sound wenzelm@44967: translations, support for more provers (Waldmeister, LEO-II, wenzelm@44967: Satallax). Further development of Nitpick and 'try' command. wenzelm@44967: wenzelm@44967: * 2011: Andreas Lochbihler, Karlsruhe Institute of Technology wenzelm@44967: Theory HOL/Library/Cset_Monad allows do notation for computable sets wenzelm@44967: (cset) via the generic monad ad-hoc overloading facility. wenzelm@44967: wenzelm@44967: * 2011: Johannes Hölzl, Armin Heller, TUM and wenzelm@44967: Bogdan Grechuk, University of Edinburgh wenzelm@44967: Theory HOL/Library/Extended_Reals: real numbers extended with plus wenzelm@44967: and minus infinity. wenzelm@44967: wenzelm@44882: * 2011: Makarius Wenzel, Université Paris-Sud / LRI wenzelm@44882: Various building blocks for Isabelle/Scala layer and Isabelle/jEdit wenzelm@44882: Prover IDE. wenzelm@44882: huffman@44908: 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. blanchet@48977: 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.