wenzelm@24799: For the purposes of the license agreement in the file COPYRIGHT, a wenzelm@62098: 'contributor' is anybody who is listed in this file (CONTRIBUTORS) or who is wenzelm@62098: listed as an author in one of the source files of this Isabelle distribution. wenzelm@62098: kleing@23382: wenzelm@68391: Contributions to Isabelle2018 wenzelm@68391: ----------------------------- wenzelm@66651: immler@68522: * June 2018: Fabian Immler immler@68522: More tool support for HOL-Types_To_Sets. immler@68522: lp15@68466: * June 2018: Martin Baillon and Paulo Emílio de Vilhena lp15@68466: A variety of contributions to HOL-Algebra. lp15@68466: eberlm@68246: * May 2018: Manuel Eberl wenzelm@68391: Landau symbols and asymptotic equivalence (moved from the AFP). eberlm@68246: immler@68073: * May 2018: Jose Divasón (Universidad de la Rioja), immler@68072: Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam), immler@68072: Fabian Immler (TUM) immler@68072: Generalizations in the formalization of linear algebra. immler@68072: haftmann@68028: * May 2018: Florian Haftmann haftmann@68028: Consolidation of string-like types in HOL. haftmann@68028: Andreas@68200: * May 2018: Andreas Lochbihler (Digital Asset), Andreas@68200: Pascal Stoop (ETH Zurich) Andreas@68200: Code generation with lazy evaluation semantics. Andreas@68200: haftmann@67928: * March 2018: Florian Haftmann wenzelm@68391: Abstract bit operations push_bit, take_bit, drop_bit, alongside with an wenzelm@68391: algebraic foundation for bit strings and word types in HOL-ex. haftmann@67928: eberlm@67831: * March 2018: Viorel Preoteasa eberlm@67831: Generalisation of complete_distrib_lattice eberlm@67831: nipkow@67456: * January 2018: Sebastien Gouezel nipkow@67456: Various small additions to HOL-Analysis nipkow@67456: traytel@67224: * December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel haftmann@67279: A new conditional parametricity prover. traytel@67224: nipkow@66893: * October 2017: Alexander Maletzky wenzelm@68391: Derivation of axiom "iff" in theory HOL.HOL from the other axioms. wenzelm@68391: wenzelm@66651: wenzelm@66475: Contributions to Isabelle2017 wenzelm@66482: ----------------------------- wenzelm@64439: wenzelm@66648: * September 2017: Lawrence Paulson wenzelm@66648: HOL-Analysis, e.g. simplicial complexes, Jordan Curve Theorem. wenzelm@66648: wenzelm@66648: * September 2017: Jasmin Blanchette wenzelm@66648: Further integration of Nunchaku model finder. wenzelm@66648: wenzelm@66475: * November 2016 - June 2017: Makarius Wenzel wenzelm@66475: New Isabelle/VSCode, with underlying restructuring of Isabelle/PIDE. wenzelm@66475: wenzelm@66475: * 2017: Makarius Wenzel wenzelm@66475: Session-qualified theory names (theory imports and ROOT files). wenzelm@66475: Prover IDE improvements. wenzelm@66475: Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL. wenzelm@66475: Andreas@66563: * August 2017: Andreas Lochbihler, ETH Zurich Andreas@66563: type of unordered pairs (HOL-Library.Uprod) Andreas@66563: eberlm@66480: * August 2017: Manuel Eberl, TUM eberlm@66480: HOL-Analysis: infinite products over natural numbers, eberlm@66480: infinite sums over arbitrary sets, connection between formal eberlm@66480: power series and analytic complex functions eberlm@66480: ballarin@65330: * March 2017: Alasdair Armstrong, University of Sheffield and ballarin@65330: Simon Foster, University of York ballarin@65099: Fixed-point theory and Galois Connections in HOL-Algebra. ballarin@65099: haftmann@65041: * February 2017: Florian Haftmann, TUM haftmann@65042: Statically embedded computations implemented by generated code. haftmann@65041: wenzelm@64439: wenzelm@64072: Contributions to Isabelle2016-1 wenzelm@64072: ------------------------------- wenzelm@62216: wenzelm@64551: * December 2016: Ondřej Kunčar, TUM wenzelm@64551: Types_To_Sets: experimental extension of Higher-Order Logic to allow wenzelm@64551: translation of types to sets. wenzelm@64551: wenzelm@64393: * October 2016: Jasmin Blanchette wenzelm@64393: Integration of Nunchaku model finder. wenzelm@64393: wenzelm@64393: * October 2016: Jaime Mendizabal Roche, TUM wenzelm@64393: Ported remaining theories of session Old_Number_Theory to the new wenzelm@64393: Number_Theory and removed Old_Number_Theory. wenzelm@64393: wenzelm@64393: * September 2016: Sascha Boehme wenzelm@64393: Proof method "argo" based on SMT technology for a combination of wenzelm@64393: quantifier-free propositional logic, equality and linear real arithmetic wenzelm@64393: wenzelm@64393: * July 2016: Daniel Stuewe wenzelm@64393: Height-size proofs in HOL-Data_Structures. wenzelm@64393: wenzelm@64393: * July 2016: Manuel Eberl, TUM wenzelm@64393: Algebraic foundation for primes; generalization from nat to general wenzelm@64393: factorial rings. wenzelm@64393: wenzelm@64393: * June 2016: Andreas Lochbihler, ETH Zurich wenzelm@64393: Formalisation of discrete subprobability distributions. wenzelm@64393: wenzelm@64393: * June 2016: Florian Haftmann, TUM wenzelm@64393: Improvements to code generation: optional timing measurements, more succint wenzelm@64393: closures for static evaluation, less ambiguities concering Scala implicits. wenzelm@64393: wenzelm@64393: * May 2016: Manuel Eberl, TUM wenzelm@64393: Code generation for Probability Mass Functions. haftmann@62343: haftmann@64011: * March 2016: Florian Haftmann, TUM haftmann@62499: Abstract factorial rings with unique factorization. haftmann@62499: haftmann@64011: * March 2016: Florian Haftmann, TUM wenzelm@64393: Reworking of the HOL char type as special case of a finite numeral type. wenzelm@62216: wenzelm@64393: * March 2016: Andreas Lochbihler, ETH Zurich wenzelm@64393: Reasoning support for monotonicity, continuity and admissibility in wenzelm@64393: chain-complete partial orders. haftmann@64011: wenzelm@64393: * February - October 2016: Makarius Wenzel wenzelm@64393: Prover IDE improvements. wenzelm@64393: ML IDE improvements: bootstrap of Pure. wenzelm@64393: Isar language consolidation. wenzelm@64393: Notational modernization of HOL. wenzelm@64393: Tight Poly/ML integration. wenzelm@64393: More Isabelle/Scala system programming modules (e.g. SSH, Mercurial). eberlm@63552: blanchet@64433: * Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy, blanchet@64433: Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu, blanchet@64433: Middlesex University, and Dmitriy Traytel, ETH Zurich blanchet@64433: 'corec' command and friends. blanchet@64433: wenzelm@64393: * January 2016: Florian Haftmann, TUM wenzelm@64393: Abolition of compound operators INFIMUM and SUPREMUM for complete lattices. blanchet@64389: blanchet@64389: wenzelm@62016: Contributions to Isabelle2016 wenzelm@62016: ----------------------------- wenzelm@60138: eberlm@62201: * Winter 2016: Manuel Eberl, TUM eberlm@62201: Support for real exponentiation ("powr") in the "approximation" method. blanchet@62693: (This was removed in Isabelle 2015 due to a changed definition of "powr".) eberlm@62201: lp15@62138: * Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge lp15@62138: General, homology form of Cauchy's integral theorem and supporting material wenzelm@62205: (ported from HOL Light). lp15@62138: kleing@62118: * Winter 2015/16: Gerwin Klein, NICTA wenzelm@62205: New print_record command. kleing@62118: wenzelm@62236: * May - December 2015: Makarius Wenzel wenzelm@62236: Prover IDE improvements. wenzelm@62236: More Isar language elements. wenzelm@62236: Document language refinements. wenzelm@62236: Poly/ML debugger integration. wenzelm@62236: Improved multi-platform and multi-architecture support. wenzelm@62236: eberlm@62060: * Winter 2015: Manuel Eberl, TUM eberlm@62060: The radius of convergence of power series and various summability tests. wenzelm@62064: Harmonic numbers and the Euler-Mascheroni constant. eberlm@62060: The Generalised Binomial Theorem. wenzelm@62064: The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their wenzelm@62064: most important properties. lp15@62138: eberlm@62086: * Autumn 2015: Manuel Eberl, TUM eberlm@62086: Proper definition of division (with remainder) for formal power series; eberlm@62086: Euclidean Ring and GCD instance for formal power series. eberlm@62060: haftmann@61891: * Autumn 2015: Florian Haftmann, TUM wenzelm@62064: Rewrite definitions for global interpretations and sublocale declarations. haftmann@61891: Andreas@61766: * Autumn 2015: Andreas Lochbihler wenzelm@62064: Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete wenzelm@62064: partial orders. Andreas@61766: eberlm@61552: * Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl eberlm@61552: A large number of additional binomial identities. eberlm@61552: wenzelm@60632: * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel wenzelm@62064: Isar subgoal command for proof structure within unstructured proof scripts. wenzelm@60632: haftmann@60434: * Summer 2015: Florian Haftmann, TUM wenzelm@60632: Generic partial division in rings as inverse operation of multiplication. haftmann@60434: haftmann@60517: * Summer 2015: Manuel Eberl and Florian Haftmann, TUM wenzelm@62064: Type class hierarchy with common algebraic notions of integral (semi)domains wenzelm@62064: like units, associated elements and normalization wrt. units. haftmann@60517: haftmann@60804: * Summer 2015: Florian Haftmann, TUM haftmann@60804: Fundamentals of abstract type class for factorial rings. haftmann@60804: traytel@60920: * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich wenzelm@62064: Command to lift a BNF structure on the raw type to the abstract type for wenzelm@62064: typedefs. traytel@60920: wenzelm@62236: * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM wenzelm@62236: Proof of the central limit theorem: includes weak convergence, wenzelm@62236: characteristic functions, and Levy's uniqueness and continuity theorem. wenzelm@62236: wenzelm@60138: wenzelm@60012: Contributions to Isabelle2015 wenzelm@60012: ----------------------------- wenzelm@57695: wenzelm@60119: * 2014/2015: Daniel Matichuk, Toby Murray, NICTA and Makarius Wenzel wenzelm@60119: The Eisbach proof method language and "match" method. wenzelm@60119: kuncar@60260: * Winter 2014 and Spring 2015: Ondrej Kuncar, TUM wenzelm@60261: Extension of lift_definition to execute lifted functions that have as a wenzelm@60261: return type a datatype containing a subtype. kuncar@60260: wenzelm@59980: * March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII, wenzelm@59980: and Dmitriy Traytel, TUM blanchet@59813: More multiset theorems, syntax, and operations. blanchet@59813: wenzelm@59980: * December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM, and wenzelm@59980: Jeremy Avigad, Luke Serafin, CMU wenzelm@59980: Various integration theorems: mostly integration on intervals and wenzelm@59980: substitution. hoelzl@59092: haftmann@58196: * September 2014: Florian Haftmann, TUM haftmann@58196: Lexicographic order on functions and haftmann@58196: sum/product over function bodies. haftmann@58196: Andreas@58626: * August 2014: Andreas Lochbihler, ETH Zurich wenzelm@59980: Test infrastructure for executing generated code in target languages. Andreas@58626: haftmann@58023: * August 2014: Manuel Eberl, TUM wenzelm@59980: Generic euclidean algorithms for GCD et al. haftmann@58023: wenzelm@57695: wenzelm@57452: Contributions to Isabelle2014 wenzelm@57452: ----------------------------- wenzelm@54055: kleing@57513: * July 2014: Thomas Sewell, NICTA wenzelm@57516: Preserve equality hypotheses in "clarify" and friends. New wenzelm@57516: "hypsubst_thin" method configuration option. kleing@57513: haftmann@57519: * Summer 2014: Florian Haftmann, TUM haftmann@57519: Consolidation and generalization of facts concerning (abelian) haftmann@57519: semigroups and monoids, particularly products (resp. sums) on haftmann@57519: finite sets. haftmann@57419: blanchet@57216: * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM wenzelm@57452: Work on exotic automatic theorem provers for Sledgehammer (LEO-II, wenzelm@57452: veriT, Waldmeister, etc.). blanchet@57216: wenzelm@57875: * June 2014: Florian Haftmann, TUM wenzelm@57875: Internal reorganisation of the local theory / named target stack. wenzelm@57875: hoelzl@57254: * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM wenzelm@57452: Various properties of exponentially, Erlang, and normal distributed wenzelm@57452: random variables. hoelzl@57235: wenzelm@57452: * May 2014: Cezary Kaliszyk, University of Innsbruck, and wenzelm@57452: Jasmin Blanchette, TUM blanchet@57030: SML-based engines for MaSh. blanchet@57030: wenzelm@55913: * March 2014: René Thiemann nipkow@55895: Improved code generation for multisets. nipkow@55895: haftmann@56416: * February 2014: Florian Haftmann, TUM wenzelm@57452: Permanent interpretation inside theory, locale and class targets wenzelm@57452: with mixin definitions. wenzelm@57452: lp15@57474: * Spring 2014: Lawrence C Paulson, Cambridge lp15@57474: Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory lp15@57474: wenzelm@57827: * Winter 2013 and Spring 2014: Ondrej Kuncar, TUM wenzelm@57827: Various improvements to Lifting/Transfer, integration with the BNF package. wenzelm@57827: wenzelm@57452: * Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI wenzelm@57452: Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. haftmann@56416: wenzelm@57452: * Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, wenzelm@57452: Dmitriy Traytel, and Jasmin Blanchette, TUM wenzelm@57452: Various improvements to the BNF-based (co)datatype package, wenzelm@57452: including a more polished "primcorec" command, optimizations, and wenzelm@57452: integration in the "HOL" session. blanchet@56118: wenzelm@57452: * Winter/Spring 2014: Sascha Boehme, QAware GmbH, and wenzelm@57452: Jasmin Blanchette, TUM wenzelm@57452: "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and wenzelm@57452: Z3 4.3. blanchet@56118: lars@55316: * January 2014: Lars Hupel, TUM lars@55316: An improved, interactive simplifier trace with integration into the lars@55316: Isabelle/jEdit Prover IDE. wenzelm@54055: haftmann@56416: * December 2013: Florian Haftmann, TUM haftmann@56416: Consolidation of abstract interpretations concerning min and max. haftmann@56416: haftmann@56416: * November 2013: Florian Haftmann, TUM haftmann@56418: Abolition of negative numeral literals in the logic. haftmann@56416: wenzelm@55913: 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@56118: Various improvements to the 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. wenzelm@62098: wenzelm@62098: :maxLineLen=78: