wenzelm@24799: For the purposes of the license agreement in the file COPYRIGHT, a
wneuper@59324: 'contributor' is anybody who is listed in this file (CONTRIBUTORS) or who is
wneuper@59324: listed as an author in one of the source files of this Isabelle distribution.
wneuper@59324: 
wneuper@59324: 
walther@59606: Contributions to Isabelle2019
walther@59606: -----------------------------
walther@59606: 
walther@59606: * April 2019: LC Paulson
walther@59606:   Homology and supporting lemmas on topology and group theory
walther@59606: 
walther@59606: * April 2019: Paulo de Vilhena and Martin Baillon
walther@59606:   Group theory developments, esp. algebraic closure of a field
walther@59606: 
walther@59606: * February/March 2019: Makarius Wenzel
walther@59606:   Stateless management of export artifacts in the Isabelle/HOL code generator.
walther@59606: 
walther@59606: * February 2019: Manuel Eberl
walther@59606:   Exponentiation by squaring, used to implement "power" in monoid_mult and
walther@59606:   fast modular exponentiation.
walther@59606: 
walther@59606: * February 2019: Manuel Eberl
walther@59606:   Carmichael's function, primitive roots in residue rings, more properties of
walther@59606:   the order in residue rings.
walther@59606: 
walther@59606: * February 2019: Jeremy Sylvestre
walther@59606:   Formal Laurent Series and overhaul of Formal power series.
walther@59606: 
walther@59606: * January 2019: Florian Haftmann
walther@59606:   Clarified syntax and congruence rules for big operators on sets involving
walther@59606:   the image operator.
walther@59606: 
walther@59606: * January 2019: Florian Haftmann
walther@59606:   Renovation of code generation, particularly export into session data and
walther@59606:   proper strings and proper integers based on zarith for OCaml.
walther@59606: 
walther@59606: * January 2019: Andreas Lochbihler
walther@59606:   New implementation for case_of_simps based on Code_Lazy's pattern matching
walther@59606:   elimination algorithm.
walther@59606: 
walther@59606: * November/December 2018: Makarius Wenzel
walther@59606:   Support for Isabelle/Haskell applications of Isabelle/PIDE.
walther@59606: 
walther@59606: * August/September 2018: Makarius Wenzel
walther@59606:   Improvements of headless Isabelle/PIDE session and server, and systematic
walther@59606:   exports from theory documents.
walther@59606: 
walther@59606: * December 2018: Florian Haftmann
walther@59606:   Generic executable sorting algorithms based on executable comparators.
walther@59606: 
walther@59606: * October 2018: Mathias Fleury
walther@59606:   Proof reconstruction for the SMT solver veriT in the smt method.
walther@59606: 
walther@59606: 
wneuper@59451: Contributions to Isabelle2018
wneuper@59451: -----------------------------
wneuper@59451: 
wneuper@59451: * July 2018: Manuel Eberl
wneuper@59451:   "real_asymp" proof method for automatic proofs of real limits, "Big-O"
wneuper@59451:   statements, etc.
wneuper@59451: 
wneuper@59451: * June 2018: Fabian Immler
wneuper@59451:   More tool support for HOL-Types_To_Sets.
wneuper@59451: 
wneuper@59451: * June 2018: Martin Baillon and Paulo Emílio de Vilhena
wneuper@59451:   A variety of contributions to HOL-Algebra.
wneuper@59451: 
wneuper@59451: * June 2018: Wenda Li
wneuper@59451:   New/strengthened results involving analysis, topology, etc.
wneuper@59451: 
wneuper@59451: * May/June 2018: Makarius Wenzel
wneuper@59451:   System infrastructure to export blobs as theory presentation, and to dump
wneuper@59451:   PIDE database content in batch mode.
wneuper@59451: 
wneuper@59451: * May 2018: Manuel Eberl
wneuper@59451:   Landau symbols and asymptotic equivalence (moved from the AFP).
wneuper@59451: 
wneuper@59451: * May 2018: Jose Divasón (Universidad de la Rioja),
wneuper@59451:   Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
wneuper@59451:   Fabian Immler (TUM)
wneuper@59451:   Generalizations in the formalization of linear algebra.
wneuper@59451: 
wneuper@59451: * May 2018: Florian Haftmann
wneuper@59451:   Consolidation of string-like types in HOL.
wneuper@59451: 
wneuper@59451: * May 2018: Andreas Lochbihler (Digital Asset),
wneuper@59451:   Pascal Stoop (ETH Zurich)
wneuper@59451:   Code generation with lazy evaluation semantics.
wneuper@59451: 
wneuper@59451: * March 2018: Florian Haftmann
wneuper@59451:   Abstract bit operations push_bit, take_bit, drop_bit, alongside with an
wneuper@59451:   algebraic foundation for bit strings and word types in HOL-ex.
wneuper@59451: 
wneuper@59451: * March 2018: Viorel Preoteasa
wneuper@59451:   Generalisation of complete_distrib_lattice
wneuper@59451: 
wneuper@59451: * February 2018: Wenda Li
wneuper@59451:   A unified definition for the order of zeros and poles. Improved reasoning
wneuper@59451:   around non-essential singularities.
wneuper@59451: 
wneuper@59451: * January 2018: Sebastien Gouezel
wneuper@59451:   Various small additions to HOL-Analysis
wneuper@59451: 
wneuper@59451: * December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel
wneuper@59451:   A new conditional parametricity prover.
wneuper@59451: 
wneuper@59451: * October 2017: Alexander Maletzky
wneuper@59451:   Derivation of axiom "iff" in theory HOL.HOL from the other axioms.
wneuper@59451: 
wneuper@59451: 
wneuper@59324: Contributions to Isabelle2017
wneuper@59324: -----------------------------
wneuper@59324: 
wneuper@59324: * September 2017: Lawrence Paulson
wneuper@59324:   HOL-Analysis, e.g. simplicial complexes, Jordan Curve Theorem.
wneuper@59324: 
wneuper@59324: * September 2017: Jasmin Blanchette
wneuper@59324:   Further integration of Nunchaku model finder.
wneuper@59324: 
wneuper@59324: * November 2016 - June 2017: Makarius Wenzel
wneuper@59324:   New Isabelle/VSCode, with underlying restructuring of Isabelle/PIDE.
wneuper@59324: 
wneuper@59324: * 2017: Makarius Wenzel
wneuper@59324:   Session-qualified theory names (theory imports and ROOT files).
wneuper@59324:   Prover IDE improvements.
wneuper@59324:   Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL.
wneuper@59324: 
wneuper@59324: * August 2017: Andreas Lochbihler, ETH Zurich
wneuper@59324:   type of unordered pairs (HOL-Library.Uprod)
wneuper@59324: 
wneuper@59324: * August 2017: Manuel Eberl, TUM
wneuper@59324:   HOL-Analysis: infinite products over natural numbers,
wneuper@59324:   infinite sums over arbitrary sets, connection between formal
wneuper@59324:   power series and analytic complex functions
wneuper@59324: 
wneuper@59324: * March 2017: Alasdair Armstrong, University of Sheffield and
wneuper@59324:   Simon Foster, University of York
wneuper@59324:   Fixed-point theory and Galois Connections in HOL-Algebra.
wneuper@59324: 
wneuper@59324: * February 2017: Florian Haftmann, TUM
wneuper@59324:   Statically embedded computations implemented by generated code.
wneuper@59324: 
wneuper@59324: 
wneuper@59324: Contributions to Isabelle2016-1
wneuper@59324: -------------------------------
wneuper@59324: 
wneuper@59324: * December 2016: Ondřej Kunčar, TUM
wneuper@59324:   Types_To_Sets: experimental extension of Higher-Order Logic to allow
wneuper@59324:   translation of types to sets.
wneuper@59324: 
wneuper@59324: * October 2016: Jasmin Blanchette
wneuper@59324:   Integration of Nunchaku model finder.
wneuper@59324: 
wneuper@59324: * October 2016: Jaime Mendizabal Roche, TUM
wneuper@59324:   Ported remaining theories of session Old_Number_Theory to the new
wneuper@59324:   Number_Theory and removed Old_Number_Theory.
wneuper@59324: 
wneuper@59324: * September 2016: Sascha Boehme
wneuper@59324:   Proof method "argo" based on SMT technology for a combination of
wneuper@59324:   quantifier-free propositional logic, equality and linear real arithmetic
wneuper@59324: 
wneuper@59324: * July 2016: Daniel Stuewe
wneuper@59324:   Height-size proofs in HOL-Data_Structures.
wneuper@59324: 
wneuper@59324: * July 2016: Manuel Eberl, TUM
wneuper@59324:   Algebraic foundation for primes; generalization from nat to general
wneuper@59324:   factorial rings.
wneuper@59324: 
wneuper@59324: * June 2016: Andreas Lochbihler, ETH Zurich
wneuper@59324:   Formalisation of discrete subprobability distributions.
wneuper@59324: 
wneuper@59324: * June 2016: Florian Haftmann, TUM
wneuper@59324:   Improvements to code generation: optional timing measurements, more succint
wneuper@59324:   closures for static evaluation, less ambiguities concering Scala implicits.
wneuper@59324: 
wneuper@59324: * May 2016: Manuel Eberl, TUM
wneuper@59324:   Code generation for Probability Mass Functions.
wneuper@59324: 
wneuper@59324: * March 2016: Florian Haftmann, TUM
wneuper@59324:   Abstract factorial rings with unique factorization.
wneuper@59324: 
wneuper@59324: * March 2016: Florian Haftmann, TUM
wneuper@59324:   Reworking of the HOL char type as special case of a finite numeral type.
wneuper@59324: 
wneuper@59324: * March 2016: Andreas Lochbihler, ETH Zurich
wneuper@59324:   Reasoning support for monotonicity, continuity and admissibility in
wneuper@59324:   chain-complete partial orders.
wneuper@59324: 
wneuper@59324: * February - October 2016: Makarius Wenzel
wneuper@59324:   Prover IDE improvements.
wneuper@59324:   ML IDE improvements: bootstrap of Pure.
wneuper@59324:   Isar language consolidation.
wneuper@59324:   Notational modernization of HOL.
wneuper@59324:   Tight Poly/ML integration.
wneuper@59324:   More Isabelle/Scala system programming modules (e.g. SSH, Mercurial).
wneuper@59324: 
wneuper@59324: * Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy,
wneuper@59324:   Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu,
wneuper@59324:   Middlesex University, and Dmitriy Traytel, ETH Zurich
wneuper@59324:   'corec' command and friends.
wneuper@59324: 
wneuper@59324: * January 2016: Florian Haftmann, TUM
wneuper@59324:   Abolition of compound operators INFIMUM and SUPREMUM for complete lattices.
wneuper@59324: 
wneuper@59324: 
wneuper@59324: Contributions to Isabelle2016
wneuper@59324: -----------------------------
wneuper@59324: 
wneuper@59324: * Winter 2016: Manuel Eberl, TUM
wneuper@59324:   Support for real exponentiation ("powr") in the "approximation" method.
wneuper@59324:   (This was removed in Isabelle 2015 due to a changed definition of "powr".)
wneuper@59324: 
wneuper@59324: * Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge
wneuper@59324:   General, homology form of Cauchy's integral theorem and supporting material
wneuper@59324:   (ported from HOL Light).
wneuper@59324: 
wneuper@59324: * Winter 2015/16: Gerwin Klein, NICTA
wneuper@59324:   New print_record command.
wneuper@59324: 
wneuper@59324: * May - December 2015: Makarius Wenzel
wneuper@59324:   Prover IDE improvements.
wneuper@59324:   More Isar language elements.
wneuper@59324:   Document language refinements.
wneuper@59324:   Poly/ML debugger integration.
wneuper@59324:   Improved multi-platform and multi-architecture support.
wneuper@59324: 
wneuper@59324: * Winter 2015: Manuel Eberl, TUM
wneuper@59324:   The radius of convergence of power series and various summability tests.
wneuper@59324:   Harmonic numbers and the Euler-Mascheroni constant.
wneuper@59324:   The Generalised Binomial Theorem.
wneuper@59324:   The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their
wneuper@59324:   most important properties.
wneuper@59324: 
wneuper@59324: * Autumn 2015: Manuel Eberl, TUM
wneuper@59324:   Proper definition of division (with remainder) for formal power series;
wneuper@59324:   Euclidean Ring and GCD instance for formal power series.
wneuper@59324: 
wneuper@59324: * Autumn 2015: Florian Haftmann, TUM
wneuper@59324:   Rewrite definitions for global interpretations and sublocale declarations.
wneuper@59324: 
wneuper@59324: * Autumn 2015: Andreas Lochbihler
wneuper@59324:   Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete
wneuper@59324:   partial orders.
wneuper@59324: 
wneuper@59324: * Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl
wneuper@59324:   A large number of additional binomial identities.
wneuper@59324: 
wneuper@59324: * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel
wneuper@59324:   Isar subgoal command for proof structure within unstructured proof scripts.
wneuper@59324: 
wneuper@59324: * Summer 2015: Florian Haftmann, TUM
wneuper@59324:   Generic partial division in rings as inverse operation of multiplication.
wneuper@59324: 
wneuper@59324: * Summer 2015: Manuel Eberl and Florian Haftmann, TUM
wneuper@59324:   Type class hierarchy with common algebraic notions of integral (semi)domains
wneuper@59324:   like units, associated elements and normalization wrt. units.
wneuper@59324: 
wneuper@59324: * Summer 2015: Florian Haftmann, TUM
wneuper@59324:   Fundamentals of abstract type class for factorial rings.
wneuper@59324: 
wneuper@59324: * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich
wneuper@59324:   Command to lift a BNF structure on the raw type to the abstract type for
wneuper@59324:   typedefs.
wneuper@59324: 
wneuper@59324: * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
wneuper@59324:   Proof of the central limit theorem: includes weak convergence,
wneuper@59324:   characteristic functions, and Levy's uniqueness and continuity theorem.
wneuper@59324: 
kleing@23382: 
wneuper@59180: Contributions to Isabelle2015
wneuper@59180: -----------------------------
wneuper@59180: 
wneuper@59180: * 2014/2015: Daniel Matichuk, Toby Murray, NICTA and Makarius Wenzel
wneuper@59180:   The Eisbach proof method language and "match" method.
wneuper@59180: 
wneuper@59180: * Winter 2014 and Spring 2015: Ondrej Kuncar, TUM
wneuper@59180:   Extension of lift_definition to execute lifted functions that have as a
wneuper@59180:   return type a datatype containing a subtype.
wneuper@59180: 
wneuper@59180: * March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII,
wneuper@59180:   and Dmitriy Traytel, TUM
wneuper@59180:   More multiset theorems, syntax, and operations.
wneuper@59180: 
wneuper@59180: * December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM, and
wneuper@59180:   Jeremy Avigad, Luke Serafin, CMU
wneuper@59180:   Various integration theorems: mostly integration on intervals and
wneuper@59180:   substitution.
wneuper@59180: 
wneuper@59180: * September 2014: Florian Haftmann, TUM
wneuper@59180:   Lexicographic order on functions and
wneuper@59180:   sum/product over function bodies.
wneuper@59180: 
wneuper@59180: * August 2014: Andreas Lochbihler, ETH Zurich
wneuper@59180:   Test infrastructure for executing generated code in target languages.
wneuper@59180: 
wneuper@59180: * August 2014: Manuel Eberl, TUM
wneuper@59180:   Generic euclidean algorithms for GCD et al.
wneuper@59180: 
wneuper@59180: 
wenzelm@58794: Contributions to Isabelle2014
wenzelm@58794: -----------------------------
wenzelm@55507: 
kleing@58855: * July 2014: Thomas Sewell, NICTA
wenzelm@58858:   Preserve equality hypotheses in "clarify" and friends. New
wenzelm@58858:   "hypsubst_thin" method configuration option.
kleing@58855: 
haftmann@58861: * Summer 2014: Florian Haftmann, TUM
haftmann@58861:   Consolidation and generalization of facts concerning (abelian)
haftmann@58861:   semigroups and monoids, particularly products (resp. sums) on
haftmann@58861:   finite sets.
haftmann@58761: 
blanchet@58558: * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM
wenzelm@58794:   Work on exotic automatic theorem provers for Sledgehammer (LEO-II,
wenzelm@58794:   veriT, Waldmeister, etc.).
blanchet@58558: 
wenzelm@59091: * June 2014: Florian Haftmann, TUM
wenzelm@59091:   Internal reorganisation of the local theory / named target stack.
wenzelm@59091: 
hoelzl@58596: * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM
wenzelm@58794:   Various properties of exponentially, Erlang, and normal distributed
wenzelm@58794:   random variables.
hoelzl@58577: 
wenzelm@58794: * May 2014: Cezary Kaliszyk, University of Innsbruck, and
wenzelm@58794:   Jasmin Blanchette, TUM
blanchet@58372:   SML-based engines for MaSh.
blanchet@58372: 
wenzelm@57255: * March 2014: René Thiemann
nipkow@57237:   Improved code generation for multisets.
nipkow@57237: 
haftmann@57758: * February 2014: Florian Haftmann, TUM
wenzelm@58794:   Permanent interpretation inside theory, locale and class targets
wenzelm@58794:   with mixin definitions.
haftmann@57758: 
lp15@58816: * Spring 2014: Lawrence C Paulson, Cambridge
lp15@58816:   Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory
lp15@58816: 
wenzelm@59043: * Winter 2013 and Spring 2014: Ondrej Kuncar, TUM
wenzelm@59043:   Various improvements to Lifting/Transfer, integration with the BNF package.
wenzelm@59043: 
wenzelm@58794: * Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI
wenzelm@58794:   Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
blanchet@57460: 
wenzelm@58794: * Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny,
wenzelm@58794:   Dmitriy Traytel, and Jasmin Blanchette, TUM
wenzelm@58794:   Various improvements to the BNF-based (co)datatype package,
wenzelm@58794:   including a more polished "primcorec" command, optimizations, and
wenzelm@58794:   integration in the "HOL" session.
wenzelm@58794: 
wenzelm@58794: * Winter/Spring 2014: Sascha Boehme, QAware GmbH, and
wenzelm@58794:   Jasmin Blanchette, TUM
wenzelm@58794:   "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and
wenzelm@58794:   Z3 4.3.
blanchet@57460: 
lars@56658: * January 2014: Lars Hupel, TUM
lars@56658:   An improved, interactive simplifier trace with integration into the
lars@56658:   Isabelle/jEdit Prover IDE.
wenzelm@55507: 
haftmann@57758: * December 2013: Florian Haftmann, TUM
haftmann@57758:   Consolidation of abstract interpretations concerning min and max.
haftmann@57758: 
haftmann@57758: * November 2013: Florian Haftmann, TUM
haftmann@57760:   Abolition of negative numeral literals in the logic.
haftmann@57758: 
wenzelm@57255: 
wenzelm@55121: Contributions to Isabelle2013-1
wenzelm@55121: -------------------------------
wenzelm@52176: 
noschinl@55251: * September 2013: Lars Noschinski, TUM
wenzelm@55252:   Conversion between function definitions as list of equations and
wenzelm@55252:   case expressions in HOL.
wenzelm@55252:   New library Simps_Case_Conv with commands case_of_simps,
wenzelm@55252:   simps_of_case.
noschinl@55251: 
wenzelm@54533: * September 2013: Nik Sultana, University of Cambridge
wenzelm@54533:   Improvements to HOL/TPTP parser and import facilities.
wenzelm@54533: 
traytel@55166: * September 2013: Johannes Hölzl and Dmitriy Traytel, TUM
traytel@55166:   New "coinduction" method (residing in HOL-BNF) to avoid boilerplate.
traytel@55166: 
wenzelm@55121: * Summer 2013: Makarius Wenzel, Université Paris-Sud / LRI
wenzelm@55121:   Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
wenzelm@55121: 
krauss@54750: * Summer 2013: Manuel Eberl, TUM
krauss@54750:   Generation of elimination rules in the function package.
krauss@54750:   New command "fun_cases".
krauss@54750: 
wenzelm@55188: * Summer 2013: Christian Sternagel, JAIST
wenzelm@55188:   Improved support for ad hoc overloading of constants, including
wenzelm@55188:   documentation and examples.
wenzelm@55188: 
wenzelm@54533: * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and
wenzelm@54533:   Jasmin Blanchette, TUM
blanchet@57460:   Various improvements to the BNF-based (co)datatype package, including
blanchet@55147:   "primrec_new" and "primcorec" commands and a compatibility layer.
blanchet@54444: 
kuncar@55158: * Spring and Summer 2013: Ondrej Kuncar, TUM
wenzelm@55172:   Various improvements of Lifting and Transfer packages.
kuncar@55158: 
kuncar@55158: * Spring 2013: Brian Huffman, Galois Inc.
wenzelm@55172:   Improvements of the Transfer package.
wenzelm@55188: 
blanchet@54865: * Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen
blanchet@54865:   Jasmin Blanchette, TUM
blanchet@54865:   Various improvements to MaSh, including a server mode.
blanchet@54865: 
blanchet@54865: * First half of 2013: Steffen Smolka, TUM
blanchet@54865:   Further improvements to Sledgehammer's Isar proof generator.
blanchet@54865: 
haftmann@53622: * May 2013: Florian Haftmann, TUM
haftmann@53622:   Ephemeral interpretation in local theories.
haftmann@53622: 
bulwahn@53403: * May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM
wenzelm@54301:   Spec_Check: A Quickcheck tool for Isabelle/ML.
bulwahn@53403: 
traytel@52819: * April 2013: Stefan Berghofer, secunet Security Networks AG
traytel@52819:   Dmitriy Traytel, TUM
traytel@52819:   Makarius Wenzel, Université Paris-Sud / LRI
traytel@52819:   Case translations as a separate check phase independent of the
traytel@52819:   datatype package.
traytel@52819: 
haftmann@52624: * March 2013: Florian Haftmann, TUM
haftmann@52626:   Reform of "big operators" on sets.
haftmann@52626: 
haftmann@52626: * March 2013: Florian Haftmann, TUM
haftmann@52624:   Algebraic locale hierarchy for orderings and (semi)lattices.
haftmann@52624: 
wenzelm@53640: * February 2013: Florian Haftmann, TUM
wenzelm@53640:   Reworking and consolidation of code generation for target language
wenzelm@53640:   numerals.
haftmann@52304: 
wenzelm@53640: * February 2013: Florian Haftmann, TUM
haftmann@52310:   Sieve of Eratosthenes.
haftmann@52310: 
haftmann@52304: 
wenzelm@52008: Contributions to Isabelle2013
wenzelm@52008: -----------------------------
wenzelm@48902: 
wenzelm@50547: * 2012: Makarius Wenzel, Université Paris-Sud / LRI
wenzelm@50547:   Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
wenzelm@50547: 
wenzelm@51663: * Fall 2012: Daniel Kühlwein, ICIS, Radboud University Nijmegen
blanchet@51237:   Jasmin Blanchette, TUM
blanchet@51237:   Implemented Machine Learning for Sledgehammer (MaSh).
blanchet@51237: 
blanchet@51234: * Fall 2012: Steffen Smolka, TUM
wenzelm@51663:   Various improvements to Sledgehammer's Isar proof generator,
wenzelm@51663:   including a smart type annotation algorithm and proof shrinking.
blanchet@51234: 
nipkow@51588: * December 2012: Alessandro Coglio, Kestrel
wenzelm@52006:   Contributions to HOL's Lattice library.
nipkow@51588: 
hoelzl@51157: * November 2012: Fabian Immler, TUM
wenzelm@51199:   "Symbols" dockable for Isabelle/jEdit.
wenzelm@51199: 
wenzelm@51199: * November 2012: Fabian Immler, TUM
wenzelm@51199:   Proof of the Daniell-Kolmogorov theorem: the existence of the limit
wenzelm@51199:   of projective families.
hoelzl@51157: 
Andreas@50785: * October 2012: Andreas Lochbihler, KIT
wenzelm@51199:   Efficient construction of red-black trees from sorted associative
wenzelm@51199:   lists.
Andreas@50785: 
haftmann@50205: * September 2012: Florian Haftmann, TUM
haftmann@50205:   Lattice instances for type option.
haftmann@50205: 
Christian@50160: * September 2012: Christian Sternagel, JAIST
Christian@50160:   Consolidated HOL/Library (theories: Prefix_Order, Sublist, and
Christian@50160:   Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists.
Christian@50160: 
blanchet@49992: * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM
blanchet@50525:   New BNF-based (co)datatype package.
blanchet@49992: 
blanchet@49992: * August 2012: Andrei Popescu and Dmitriy Traytel, TUM
blanchet@49992:   Theories of ordinals and cardinals.
blanchet@49992: 
wenzelm@49600: * July 2012: Makarius Wenzel, Université Paris-Sud / LRI
wenzelm@49600:   Advanced support for Isabelle sessions and build management, notably
wenzelm@49600:   "isabelle build".
wenzelm@49600: 
bulwahn@49126: * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
wenzelm@49600:   Simproc for rewriting set comprehensions into pointfree expressions.
wenzelm@48902: 
Andreas@50496: * May 2012: Andreas Lochbihler, KIT
Andreas@50496:   Theory of almost everywhere constant functions.
wenzelm@49139: 
wenzelm@51663: * 2010-2012: Markus Kaiser and Lukas Bulwahn, TUM
wenzelm@51663:   Graphview in Scala/Swing.
wenzelm@51663: 
wenzelm@51663: 
wenzelm@48333: Contributions to Isabelle2012
wenzelm@48333: -----------------------------
wenzelm@45961: 
hoelzl@48566: * April 2012: Johannes Hölzl, TUM
wenzelm@48679:   Probability: Introduced type to represent measures instead of
wenzelm@48679:   locales.
hoelzl@48566: 
hoelzl@48566: * April 2012: Johannes Hölzl, Fabian Immler, TUM
hoelzl@48566:   Float: Moved to Dyadic rationals to represent floating point numers.
hoelzl@48566: 
wenzelm@48679: * April 2012: Thomas Sewell, NICTA and
wenzelm@48679:   2010: Sascha Boehme, TUM
wenzelm@48679:   Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector
wenzelm@48679:   equalities/inequalities.
thomas@48438: 
wenzelm@48679: * March 2012: Christian Sternagel, JAIST
bulwahn@48319:   Consolidated theory of relation composition.
bulwahn@48319: 
wenzelm@48284: * March 2012: Nik Sultana, University of Cambridge
wenzelm@48284:   HOL/TPTP parser and import facilities.
wenzelm@48284: 
wenzelm@48333: * March 2012: Cezary Kaliszyk, University of Innsbruck and
wenzelm@48333:   Alexander Krauss, QAware GmbH
wenzelm@48333:   Faster and more scalable Import mechanism for HOL Light proofs.
wenzelm@48333: 
blanchet@48434: * January 2012: Florian Haftmann, TUM, et al.
haftmann@47467:   (Re-)Introduction of the "set" type constructor.
haftmann@47467: 
kuncar@48571: * 2012: Ondrej Kuncar, TUM
wenzelm@48679:   New package Lifting, various improvements and refinements to the
wenzelm@48679:   Quotient package.
kuncar@48571: 
blanchet@48434: * 2011/2012: Jasmin Blanchette, TUM
blanchet@48434:   Various improvements to Sledgehammer, notably: tighter integration
wenzelm@48679:   with SPASS, support for more provers (Alt-Ergo, iProver,
wenzelm@48679:   iProver-Eq).
blanchet@48434: 
wenzelm@48333: * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI
wenzelm@48356:   Various refinements of local theory infrastructure.
wenzelm@48333:   Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE.
krauss@48136: 
wenzelm@45961: 
wenzelm@45682: Contributions to Isabelle2011-1
wenzelm@45682: -------------------------------
wenzelm@42520: 
haftmann@45680: * September 2011: Peter Gammie
huffman@45779:   Theory HOL/Library/Saturated: numbers with saturated arithmetic.
haftmann@45680: 
haftmann@45680: * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
haftmann@45680:   Refined theory on complete lattices.
haftmann@45680: 
wenzelm@45838: * August 2011: Brian Huffman, Portland State University
wenzelm@45838:   Miscellaneous cleanup of Complex_Main and Multivariate_Analysis.
wenzelm@45838: 
wenzelm@45838: * June 2011: Brian Huffman, Portland State University
wenzelm@45838:   Proof method "countable_datatype" for theory Library/Countable.
wenzelm@45838: 
wenzelm@45838: * 2011: Jasmin Blanchette, TUM
wenzelm@45838:   Various improvements to Sledgehammer, notably: use of sound
wenzelm@45838:   translations, support for more provers (Waldmeister, LEO-II,
wenzelm@45838:   Satallax). Further development of Nitpick and 'try' command.
wenzelm@45838: 
wenzelm@45838: * 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
wenzelm@45838:   Theory HOL/Library/Cset_Monad allows do notation for computable sets
wenzelm@45838:   (cset) via the generic monad ad-hoc overloading facility.
wenzelm@45838: 
wenzelm@45838: * 2011: Johannes Hölzl, Armin Heller, TUM and
wenzelm@45838:   Bogdan Grechuk, University of Edinburgh
wenzelm@45838:   Theory HOL/Library/Extended_Reals: real numbers extended with plus
wenzelm@45838:   and minus infinity.
wenzelm@45838: 
wenzelm@45756: * 2011: Makarius Wenzel, Université Paris-Sud / LRI
wenzelm@45756:   Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
wenzelm@45756:   Prover IDE.
wenzelm@45756: 
huffman@45779: 
wenzelm@41760: Contributions to Isabelle2011
wenzelm@41760: -----------------------------
wenzelm@37358: 
berghofe@41815: * January 2011: Stefan Berghofer, secunet Security Networks AG
berghofe@41815:   HOL-SPARK: an interactive prover back-end for SPARK.
berghofe@41815: 
wenzelm@40625: * October 2010: Bogdan Grechuk, University of Edinburgh
wenzelm@40625:   Extended convex analysis in Multivariate Analysis.
wenzelm@40625: 
wenzelm@40534: * October 2010: Dmitriy Traytel, TUM
wenzelm@40534:   Coercive subtyping via subtype constraints.
wenzelm@40534: 
krauss@41779: * October 2010: Alexander Krauss, TUM
krauss@41779:   Command partial_function for function definitions based on complete
krauss@41779:   partial orders in HOL.
krauss@41779: 
haftmann@39868: * September 2010: Florian Haftmann, TUM
wenzelm@41844:   Refined concepts for evaluation, i.e., normalization of terms using
krauss@41779:   different techniques.
haftmann@40364: 
haftmann@40364: * September 2010: Florian Haftmann, TUM
haftmann@39868:   Code generation for Scala.
haftmann@39868: 
hoelzl@38902: * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
wenzelm@41844:   Improved Probability theory in HOL.
hoelzl@38902: 
haftmann@38705: * July 2010: Florian Haftmann, TUM
haftmann@39868:   Reworking and extension of the Imperative HOL framework.
haftmann@38705: 
wenzelm@41844: * July 2010: Alexander Krauss, TUM and Christian Sternagel, University
wenzelm@41844:     of Innsbruck
krauss@41779:   Ad-hoc overloading. Generic do notation for monads.
krauss@41779: 
wenzelm@37358: 
wenzelm@37144: Contributions to Isabelle2009-2
wenzelm@41760: -------------------------------
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@49992: 
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@33408: 
blanchet@33192: * October 2009: Jasmin Blanchette, TUM
wenzelm@33842:   Nitpick: yet another counterexample generator for Isabelle/HOL.
blanchet@33192: 
boehmes@33006: * October 2009: Sascha Boehme, TUM
wenzelm@33182:   Extension of SMT method: proof-reconstruction for the SMT solver Z3.
boehmes@33006: 
boehmes@33006: * October 2009: Florian Haftmann, TUM
wenzelm@33182:   Refinement of parts of the HOL datatype package.
haftmann@33002: 
boehmes@33006: * October 2009: Florian Haftmann, TUM
wenzelm@33182:   Generic term styles for term antiquotations.
haftmann@33002: 
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@32265: * July 2009: Philipp Meyer, TUM
wenzelm@33182:   HOL/Library/Sum_Of_Squares: functionality to call a remote csdp
wenzelm@33182:   prover.
Philipp@32265: 
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@39868:   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@30979: 
Philipp@32265: * March 2009: Philipp Meyer, TUM
wenzelm@33843:   Minimization tool for results from Sledgehammer.
wenzelm@33182: 
Philipp@32265: 
wenzelm@30979: Contributions to Isabelle2009
wenzelm@30979: -----------------------------
wenzelm@30979: 
wenzelm@30388: * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
wenzelm@30388:   Cambridge
wenzelm@30388:   Elementary topology in Euclidean space.
wenzelm@30388: 
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@29820:   New find_consts command.
kleing@29820: 
wenzelm@30162: * February 2009: Timothy Bourke, NICTA
kleing@29798:   "solves" criterion for find_theorems and auto_solve option
kleing@29798: 
haftmann@29395: * December 2008: Clemens Ballarin, TUM
haftmann@29395:   New locale implementation.
haftmann@29395: 
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@29395: * 2008: Florian Haftmann, TUM
haftmann@29395:   Various extensions and restructurings in HOL, improvements
haftmann@29395:   in evaluation mechanisms, new module binding.ML for name bindings.
haftmann@29395: 
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.
paulson@23449: 
wenzelm@24799: * 2007: Kong W. Susanto, Cambridge
paulson@23449:   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.
wenzelm@24799: 
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.
wneuper@59324: 
wneuper@59324: :maxLineLen=78: