CONTRIBUTORS

executable equality

For the purposes of the license agreement in the file COPYRIGHT, a
'contributor' is anybody who is listed in this file (CONTRIBUTORS) or who is
listed as an author in one of the source files of this Isabelle distribution.


Contributions to this Isabelle version
--------------------------------------

* January 2019: Florian Haftmann
  Clarified syntax and congruence rules for big operators on sets
  involving the image operator.

* January 2919: Florian Haftmann
  Renovation of code generation, particularly export into session data
  and proper strings and proper integers based on zarith for OCaml.

* February 2019: Jeremy Sylvestre
  Formal Laurent Series and overhaul of Formal power series.

* February 2019: Manuel Eberl
  Exponentiation by squaring, used to implement "power" in monoid_mult and
  fast modular exponentiation.

* February 2019: Manuel Eberl
  Carmichael's function, primitive roots in residue rings, more properties
  of the order in residue rings.

* January 2019: Andreas Lochbihler
  New implementation for case_of_simps based on Code_Lazy's
  pattern matching elimination algorithm.

* December 2018: Florian Haftmann
  Generic executable sorting algorithms based on executable comparators.

* October 2018: Mathias Fleury
  Proof reconstruction for the SMT solver veriT in the smt method.


Contributions to Isabelle2018
-----------------------------

* July 2018: Manuel Eberl
  "real_asymp" proof method for automatic proofs of real limits, "Big-O"
  statements, etc.

* June 2018: Fabian Immler
  More tool support for HOL-Types_To_Sets.

* June 2018: Martin Baillon and Paulo Emílio de Vilhena
  A variety of contributions to HOL-Algebra.

* June 2018: Wenda Li
  New/strengthened results involving analysis, topology, etc.

* May/June 2018: Makarius Wenzel
  System infrastructure to export blobs as theory presentation, and to dump
  PIDE database content in batch mode.

* May 2018: Manuel Eberl
  Landau symbols and asymptotic equivalence (moved from the AFP).

* May 2018: Jose Divasón (Universidad de la Rioja),
  Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
  Fabian Immler (TUM)
  Generalizations in the formalization of linear algebra.

* May 2018: Florian Haftmann
  Consolidation of string-like types in HOL.

* May 2018: Andreas Lochbihler (Digital Asset),
  Pascal Stoop (ETH Zurich)
  Code generation with lazy evaluation semantics.

* March 2018: Florian Haftmann
  Abstract bit operations push_bit, take_bit, drop_bit, alongside with an
  algebraic foundation for bit strings and word types in HOL-ex.

* March 2018: Viorel Preoteasa
  Generalisation of complete_distrib_lattice

* February 2018: Wenda Li
  A unified definition for the order of zeros and poles. Improved reasoning
  around non-essential singularities.

* January 2018: Sebastien Gouezel
  Various small additions to HOL-Analysis

* December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel
  A new conditional parametricity prover.

* October 2017: Alexander Maletzky
  Derivation of axiom "iff" in theory HOL.HOL from the other axioms.


Contributions to Isabelle2017
-----------------------------

* September 2017: Lawrence Paulson
  HOL-Analysis, e.g. simplicial complexes, Jordan Curve Theorem.

* September 2017: Jasmin Blanchette
  Further integration of Nunchaku model finder.

* November 2016 - June 2017: Makarius Wenzel
  New Isabelle/VSCode, with underlying restructuring of Isabelle/PIDE.

* 2017: Makarius Wenzel
  Session-qualified theory names (theory imports and ROOT files).
  Prover IDE improvements.
  Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL.

* August 2017: Andreas Lochbihler, ETH Zurich
  type of unordered pairs (HOL-Library.Uprod)

* August 2017: Manuel Eberl, TUM
  HOL-Analysis: infinite products over natural numbers,
  infinite sums over arbitrary sets, connection between formal
  power series and analytic complex functions

* March 2017: Alasdair Armstrong, University of Sheffield and
  Simon Foster, University of York
  Fixed-point theory and Galois Connections in HOL-Algebra.

* February 2017: Florian Haftmann, TUM
  Statically embedded computations implemented by generated code.


Contributions to Isabelle2016-1
-------------------------------

* December 2016: Ondřej Kunčar, TUM
  Types_To_Sets: experimental extension of Higher-Order Logic to allow
  translation of types to sets.

* October 2016: Jasmin Blanchette
  Integration of Nunchaku model finder.

* October 2016: Jaime Mendizabal Roche, TUM
  Ported remaining theories of session Old_Number_Theory to the new
  Number_Theory and removed Old_Number_Theory.

* September 2016: Sascha Boehme
  Proof method "argo" based on SMT technology for a combination of
  quantifier-free propositional logic, equality and linear real arithmetic

* July 2016: Daniel Stuewe
  Height-size proofs in HOL-Data_Structures.

* July 2016: Manuel Eberl, TUM
  Algebraic foundation for primes; generalization from nat to general
  factorial rings.

* June 2016: Andreas Lochbihler, ETH Zurich
  Formalisation of discrete subprobability distributions.

* June 2016: Florian Haftmann, TUM
  Improvements to code generation: optional timing measurements, more succint
  closures for static evaluation, less ambiguities concering Scala implicits.