CONTRIBUTORS
author haftmann
Fri Jun 14 12:29:50 2019 +0200 (2 months ago)
changeset 70351 32b4e1aec5ca
parent 70265 a8238fd25541
permissions -rw-r--r--
make latex happy
     1 For the purposes of the license agreement in the file COPYRIGHT, a
     2 'contributor' is anybody who is listed in this file (CONTRIBUTORS) or who is
     3 listed as an author in one of the source files of this Isabelle distribution.
     4 
     5 
     6 Contributions to this Isabelle version
     7 --------------------------------------
     8 
     9 
    10 Contributions to Isabelle2019
    11 -----------------------------
    12 
    13 * April 2019: LC Paulson
    14   Homology and supporting lemmas on topology and group theory
    15 
    16 * April 2019: Paulo de Vilhena and Martin Baillon
    17   Group theory developments, esp. algebraic closure of a field
    18 
    19 * February/March 2019: Makarius Wenzel
    20   Stateless management of export artifacts in the Isabelle/HOL code generator.
    21 
    22 * February 2019: Manuel Eberl
    23   Exponentiation by squaring, used to implement "power" in monoid_mult and
    24   fast modular exponentiation.
    25 
    26 * February 2019: Manuel Eberl
    27   Carmichael's function, primitive roots in residue rings, more properties of
    28   the order in residue rings.
    29 
    30 * February 2019: Jeremy Sylvestre
    31   Formal Laurent Series and overhaul of Formal power series.
    32 
    33 * January 2019: Florian Haftmann
    34   Clarified syntax and congruence rules for big operators on sets involving
    35   the image operator.
    36 
    37 * January 2019: Florian Haftmann
    38   Renovation of code generation, particularly export into session data and
    39   proper strings and proper integers based on zarith for OCaml.
    40 
    41 * January 2019: Andreas Lochbihler
    42   New implementation for case_of_simps based on Code_Lazy's pattern matching
    43   elimination algorithm.
    44 
    45 * November/December 2018: Makarius Wenzel
    46   Support for Isabelle/Haskell applications of Isabelle/PIDE.
    47 
    48 * August/September 2018: Makarius Wenzel
    49   Improvements of headless Isabelle/PIDE session and server, and systematic
    50   exports from theory documents.
    51 
    52 * December 2018: Florian Haftmann
    53   Generic executable sorting algorithms based on executable comparators.
    54 
    55 * October 2018: Mathias Fleury
    56   Proof reconstruction for the SMT solver veriT in the smt method.
    57 
    58 
    59 Contributions to Isabelle2018
    60 -----------------------------
    61 
    62 * July 2018: Manuel Eberl
    63   "real_asymp" proof method for automatic proofs of real limits, "Big-O"
    64   statements, etc.
    65 
    66 * June 2018: Fabian Immler
    67   More tool support for HOL-Types_To_Sets.
    68 
    69 * June 2018: Martin Baillon and Paulo Emílio de Vilhena
    70   A variety of contributions to HOL-Algebra.
    71 
    72 * June 2018: Wenda Li
    73   New/strengthened results involving analysis, topology, etc.
    74 
    75 * May/June 2018: Makarius Wenzel
    76   System infrastructure to export blobs as theory presentation, and to dump
    77   PIDE database content in batch mode.
    78 
    79 * May 2018: Manuel Eberl
    80   Landau symbols and asymptotic equivalence (moved from the AFP).
    81 
    82 * May 2018: Jose Divasón (Universidad de la Rioja),
    83   Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam),
    84   Fabian Immler (TUM)
    85   Generalizations in the formalization of linear algebra.
    86 
    87 * May 2018: Florian Haftmann
    88   Consolidation of string-like types in HOL.
    89 
    90 * May 2018: Andreas Lochbihler (Digital Asset),
    91   Pascal Stoop (ETH Zurich)
    92   Code generation with lazy evaluation semantics.
    93 
    94 * March 2018: Florian Haftmann
    95   Abstract bit operations push_bit, take_bit, drop_bit, alongside with an
    96   algebraic foundation for bit strings and word types in HOL-ex.
    97 
    98 * March 2018: Viorel Preoteasa
    99   Generalisation of complete_distrib_lattice
   100 
   101 * February 2018: Wenda Li
   102   A unified definition for the order of zeros and poles. Improved reasoning
   103   around non-essential singularities.
   104 
   105 * January 2018: Sebastien Gouezel
   106   Various small additions to HOL-Analysis
   107 
   108 * December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel
   109   A new conditional parametricity prover.
   110 
   111 * October 2017: Alexander Maletzky
   112   Derivation of axiom "iff" in theory HOL.HOL from the other axioms.
   113 
   114 
   115 Contributions to Isabelle2017
   116 -----------------------------
   117 
   118 * September 2017: Lawrence Paulson
   119   HOL-Analysis, e.g. simplicial complexes, Jordan Curve Theorem.
   120 
   121 * September 2017: Jasmin Blanchette
   122   Further integration of Nunchaku model finder.
   123 
   124 * November 2016 - June 2017: Makarius Wenzel
   125   New Isabelle/VSCode, with underlying restructuring of Isabelle/PIDE.
   126 
   127 * 2017: Makarius Wenzel
   128   Session-qualified theory names (theory imports and ROOT files).
   129   Prover IDE improvements.
   130   Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL.
   131 
   132 * August 2017: Andreas Lochbihler, ETH Zurich
   133   type of unordered pairs (HOL-Library.Uprod)
   134 
   135 * August 2017: Manuel Eberl, TUM
   136   HOL-Analysis: infinite products over natural numbers,
   137   infinite sums over arbitrary sets, connection between formal
   138   power series and analytic complex functions
   139 
   140 * March 2017: Alasdair Armstrong, University of Sheffield and
   141   Simon Foster, University of York
   142   Fixed-point theory and Galois Connections in HOL-Algebra.
   143 
   144 * February 2017: Florian Haftmann, TUM
   145   Statically embedded computations implemented by generated code.
   146 
   147 
   148 Contributions to Isabelle2016-1
   149 -------------------------------
   150 
   151 * December 2016: Ondřej Kunčar, TUM
   152   Types_To_Sets: experimental extension of Higher-Order Logic to allow
   153   translation of types to sets.
   154 
   155 * October 2016: Jasmin Blanchette
   156   Integration of Nunchaku model finder.
   157 
   158 * October 2016: Jaime Mendizabal Roche, TUM
   159   Ported remaining theories of session Old_Number_Theory to the new
   160   Number_Theory and removed Old_Number_Theory.
   161 
   162 * September 2016: Sascha Boehme
   163   Proof method "argo" based on SMT technology for a combination of
   164   quantifier-free propositional logic, equality and linear real arithmetic
   165 
   166 * July 2016: Daniel Stuewe
   167   Height-size proofs in HOL-Data_Structures.
   168 
   169 * July 2016: Manuel Eberl, TUM
   170   Algebraic foundation for primes; generalization from nat to general
   171   factorial rings.
   172 
   173 * June 2016: Andreas Lochbihler, ETH Zurich
   174   Formalisation of discrete subprobability distributions.
   175 
   176 * June 2016: Florian Haftmann, TUM
   177   Improvements to code generation: optional timing measurements, more succint
   178   closures for static evaluation, less ambiguities concering Scala implicits.
   179 
   180 * May 2016: Manuel Eberl, TUM
   181   Code generation for Probability Mass Functions.
   182 
   183 * March 2016: Florian Haftmann, TUM
   184   Abstract factorial rings with unique factorization.
   185 
   186 * March 2016: Florian Haftmann, TUM
   187   Reworking of the HOL char type as special case of a finite numeral type.
   188 
   189 * March 2016: Andreas Lochbihler, ETH Zurich
   190   Reasoning support for monotonicity, continuity and admissibility in
   191   chain-complete partial orders.
   192 
   193 * February - October 2016: Makarius Wenzel
   194   Prover IDE improvements.
   195   ML IDE improvements: bootstrap of Pure.
   196   Isar language consolidation.
   197   Notational modernization of HOL.
   198   Tight Poly/ML integration.
   199   More Isabelle/Scala system programming modules (e.g. SSH, Mercurial).
   200 
   201 * Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy,
   202   Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu,
   203   Middlesex University, and Dmitriy Traytel, ETH Zurich
   204   'corec' command and friends.
   205 
   206 * January 2016: Florian Haftmann, TUM
   207   Abolition of compound operators INFIMUM and SUPREMUM for complete lattices.
   208 
   209 
   210 Contributions to Isabelle2016
   211 -----------------------------
   212 
   213 * Winter 2016: Manuel Eberl, TUM
   214   Support for real exponentiation ("powr") in the "approximation" method.
   215   (This was removed in Isabelle 2015 due to a changed definition of "powr".)
   216 
   217 * Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge
   218   General, homology form of Cauchy's integral theorem and supporting material
   219   (ported from HOL Light).
   220 
   221 * Winter 2015/16: Gerwin Klein, NICTA
   222   New print_record command.
   223 
   224 * May - December 2015: Makarius Wenzel
   225   Prover IDE improvements.
   226   More Isar language elements.
   227   Document language refinements.
   228   Poly/ML debugger integration.
   229   Improved multi-platform and multi-architecture support.
   230 
   231 * Winter 2015: Manuel Eberl, TUM
   232   The radius of convergence of power series and various summability tests.
   233   Harmonic numbers and the Euler-Mascheroni constant.
   234   The Generalised Binomial Theorem.
   235   The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their
   236   most important properties.
   237 
   238 * Autumn 2015: Manuel Eberl, TUM
   239   Proper definition of division (with remainder) for formal power series;
   240   Euclidean Ring and GCD instance for formal power series.
   241 
   242 * Autumn 2015: Florian Haftmann, TUM
   243   Rewrite definitions for global interpretations and sublocale declarations.
   244 
   245 * Autumn 2015: Andreas Lochbihler
   246   Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete
   247   partial orders.
   248 
   249 * Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl
   250   A large number of additional binomial identities.
   251 
   252 * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel
   253   Isar subgoal command for proof structure within unstructured proof scripts.
   254 
   255 * Summer 2015: Florian Haftmann, TUM
   256   Generic partial division in rings as inverse operation of multiplication.
   257 
   258 * Summer 2015: Manuel Eberl and Florian Haftmann, TUM
   259   Type class hierarchy with common algebraic notions of integral (semi)domains
   260   like units, associated elements and normalization wrt. units.
   261 
   262 * Summer 2015: Florian Haftmann, TUM
   263   Fundamentals of abstract type class for factorial rings.
   264 
   265 * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich
   266   Command to lift a BNF structure on the raw type to the abstract type for
   267   typedefs.
   268 
   269 * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
   270   Proof of the central limit theorem: includes weak convergence,
   271   characteristic functions, and Levy's uniqueness and continuity theorem.
   272 
   273 
   274 Contributions to Isabelle2015
   275 -----------------------------
   276 
   277 * 2014/2015: Daniel Matichuk, Toby Murray, NICTA and Makarius Wenzel
   278   The Eisbach proof method language and "match" method.
   279 
   280 * Winter 2014 and Spring 2015: Ondrej Kuncar, TUM
   281   Extension of lift_definition to execute lifted functions that have as a
   282   return type a datatype containing a subtype.
   283 
   284 * March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII,
   285   and Dmitriy Traytel, TUM
   286   More multiset theorems, syntax, and operations.
   287 
   288 * December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM, and
   289   Jeremy Avigad, Luke Serafin, CMU
   290   Various integration theorems: mostly integration on intervals and
   291   substitution.
   292 
   293 * September 2014: Florian Haftmann, TUM
   294   Lexicographic order on functions and
   295   sum/product over function bodies.
   296 
   297 * August 2014: Andreas Lochbihler, ETH Zurich
   298   Test infrastructure for executing generated code in target languages.
   299 
   300 * August 2014: Manuel Eberl, TUM
   301   Generic euclidean algorithms for GCD et al.
   302 
   303 
   304 Contributions to Isabelle2014
   305 -----------------------------
   306 
   307 * July 2014: Thomas Sewell, NICTA
   308   Preserve equality hypotheses in "clarify" and friends. New
   309   "hypsubst_thin" method configuration option.
   310 
   311 * Summer 2014: Florian Haftmann, TUM
   312   Consolidation and generalization of facts concerning (abelian)
   313   semigroups and monoids, particularly products (resp. sums) on
   314   finite sets.
   315 
   316 * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM
   317   Work on exotic automatic theorem provers for Sledgehammer (LEO-II,
   318   veriT, Waldmeister, etc.).
   319 
   320 * June 2014: Florian Haftmann, TUM
   321   Internal reorganisation of the local theory / named target stack.
   322 
   323 * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM
   324   Various properties of exponentially, Erlang, and normal distributed
   325   random variables.
   326 
   327 * May 2014: Cezary Kaliszyk, University of Innsbruck, and
   328   Jasmin Blanchette, TUM
   329   SML-based engines for MaSh.
   330 
   331 * March 2014: René Thiemann
   332   Improved code generation for multisets.
   333 
   334 * February 2014: Florian Haftmann, TUM
   335   Permanent interpretation inside theory, locale and class targets
   336   with mixin definitions.
   337 
   338 * Spring 2014: Lawrence C Paulson, Cambridge
   339   Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory
   340 
   341 * Winter 2013 and Spring 2014: Ondrej Kuncar, TUM
   342   Various improvements to Lifting/Transfer, integration with the BNF package.
   343 
   344 * Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI
   345   Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
   346 
   347 * Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny,
   348   Dmitriy Traytel, and Jasmin Blanchette, TUM
   349   Various improvements to the BNF-based (co)datatype package,
   350   including a more polished "primcorec" command, optimizations, and
   351   integration in the "HOL" session.
   352 
   353 * Winter/Spring 2014: Sascha Boehme, QAware GmbH, and
   354   Jasmin Blanchette, TUM
   355   "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and
   356   Z3 4.3.
   357 
   358 * January 2014: Lars Hupel, TUM
   359   An improved, interactive simplifier trace with integration into the
   360   Isabelle/jEdit Prover IDE.
   361 
   362 * December 2013: Florian Haftmann, TUM
   363   Consolidation of abstract interpretations concerning min and max.
   364 
   365 * November 2013: Florian Haftmann, TUM
   366   Abolition of negative numeral literals in the logic.
   367 
   368 
   369 Contributions to Isabelle2013-1
   370 -------------------------------
   371 
   372 * September 2013: Lars Noschinski, TUM
   373   Conversion between function definitions as list of equations and
   374   case expressions in HOL.
   375   New library Simps_Case_Conv with commands case_of_simps,
   376   simps_of_case.
   377 
   378 * September 2013: Nik Sultana, University of Cambridge
   379   Improvements to HOL/TPTP parser and import facilities.
   380 
   381 * September 2013: Johannes Hölzl and Dmitriy Traytel, TUM
   382   New "coinduction" method (residing in HOL-BNF) to avoid boilerplate.
   383 
   384 * Summer 2013: Makarius Wenzel, Université Paris-Sud / LRI
   385   Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
   386 
   387 * Summer 2013: Manuel Eberl, TUM
   388   Generation of elimination rules in the function package.
   389   New command "fun_cases".
   390 
   391 * Summer 2013: Christian Sternagel, JAIST
   392   Improved support for ad hoc overloading of constants, including
   393   documentation and examples.
   394 
   395 * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and
   396   Jasmin Blanchette, TUM
   397   Various improvements to the BNF-based (co)datatype package, including
   398   "primrec_new" and "primcorec" commands and a compatibility layer.
   399 
   400 * Spring and Summer 2013: Ondrej Kuncar, TUM
   401   Various improvements of Lifting and Transfer packages.
   402 
   403 * Spring 2013: Brian Huffman, Galois Inc.
   404   Improvements of the Transfer package.
   405 
   406 * Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen
   407   Jasmin Blanchette, TUM
   408   Various improvements to MaSh, including a server mode.
   409 
   410 * First half of 2013: Steffen Smolka, TUM
   411   Further improvements to Sledgehammer's Isar proof generator.
   412 
   413 * May 2013: Florian Haftmann, TUM
   414   Ephemeral interpretation in local theories.
   415 
   416 * May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM
   417   Spec_Check: A Quickcheck tool for Isabelle/ML.
   418 
   419 * April 2013: Stefan Berghofer, secunet Security Networks AG
   420   Dmitriy Traytel, TUM
   421   Makarius Wenzel, Université Paris-Sud / LRI
   422   Case translations as a separate check phase independent of the
   423   datatype package.
   424 
   425 * March 2013: Florian Haftmann, TUM
   426   Reform of "big operators" on sets.
   427 
   428 * March 2013: Florian Haftmann, TUM
   429   Algebraic locale hierarchy for orderings and (semi)lattices.
   430 
   431 * February 2013: Florian Haftmann, TUM
   432   Reworking and consolidation of code generation for target language
   433   numerals.
   434 
   435 * February 2013: Florian Haftmann, TUM
   436   Sieve of Eratosthenes.
   437 
   438 
   439 Contributions to Isabelle2013
   440 -----------------------------
   441 
   442 * 2012: Makarius Wenzel, Université Paris-Sud / LRI
   443   Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
   444 
   445 * Fall 2012: Daniel Kühlwein, ICIS, Radboud University Nijmegen
   446   Jasmin Blanchette, TUM
   447   Implemented Machine Learning for Sledgehammer (MaSh).
   448 
   449 * Fall 2012: Steffen Smolka, TUM
   450   Various improvements to Sledgehammer's Isar proof generator,
   451   including a smart type annotation algorithm and proof shrinking.
   452 
   453 * December 2012: Alessandro Coglio, Kestrel
   454   Contributions to HOL's Lattice library.
   455 
   456 * November 2012: Fabian Immler, TUM
   457   "Symbols" dockable for Isabelle/jEdit.
   458 
   459 * November 2012: Fabian Immler, TUM
   460   Proof of the Daniell-Kolmogorov theorem: the existence of the limit
   461   of projective families.
   462 
   463 * October 2012: Andreas Lochbihler, KIT
   464   Efficient construction of red-black trees from sorted associative
   465   lists.
   466 
   467 * September 2012: Florian Haftmann, TUM
   468   Lattice instances for type option.
   469 
   470 * September 2012: Christian Sternagel, JAIST
   471   Consolidated HOL/Library (theories: Prefix_Order, Sublist, and
   472   Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists.
   473 
   474 * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM
   475   New BNF-based (co)datatype package.
   476 
   477 * August 2012: Andrei Popescu and Dmitriy Traytel, TUM
   478   Theories of ordinals and cardinals.
   479 
   480 * July 2012: Makarius Wenzel, Université Paris-Sud / LRI
   481   Advanced support for Isabelle sessions and build management, notably
   482   "isabelle build".
   483 
   484 * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
   485   Simproc for rewriting set comprehensions into pointfree expressions.
   486 
   487 * May 2012: Andreas Lochbihler, KIT
   488   Theory of almost everywhere constant functions.
   489 
   490 * 2010-2012: Markus Kaiser and Lukas Bulwahn, TUM
   491   Graphview in Scala/Swing.
   492 
   493 
   494 Contributions to Isabelle2012
   495 -----------------------------
   496 
   497 * April 2012: Johannes Hölzl, TUM
   498   Probability: Introduced type to represent measures instead of
   499   locales.
   500 
   501 * April 2012: Johannes Hölzl, Fabian Immler, TUM
   502   Float: Moved to Dyadic rationals to represent floating point numers.
   503 
   504 * April 2012: Thomas Sewell, NICTA and
   505   2010: Sascha Boehme, TUM
   506   Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector
   507   equalities/inequalities.
   508 
   509 * March 2012: Christian Sternagel, JAIST
   510   Consolidated theory of relation composition.
   511 
   512 * March 2012: Nik Sultana, University of Cambridge
   513   HOL/TPTP parser and import facilities.
   514 
   515 * March 2012: Cezary Kaliszyk, University of Innsbruck and
   516   Alexander Krauss, QAware GmbH
   517   Faster and more scalable Import mechanism for HOL Light proofs.
   518 
   519 * January 2012: Florian Haftmann, TUM, et al.
   520   (Re-)Introduction of the "set" type constructor.
   521 
   522 * 2012: Ondrej Kuncar, TUM
   523   New package Lifting, various improvements and refinements to the
   524   Quotient package.
   525 
   526 * 2011/2012: Jasmin Blanchette, TUM
   527   Various improvements to Sledgehammer, notably: tighter integration
   528   with SPASS, support for more provers (Alt-Ergo, iProver,
   529   iProver-Eq).
   530 
   531 * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI
   532   Various refinements of local theory infrastructure.
   533   Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE.
   534 
   535 
   536 Contributions to Isabelle2011-1
   537 -------------------------------
   538 
   539 * September 2011: Peter Gammie
   540   Theory HOL/Library/Saturated: numbers with saturated arithmetic.
   541 
   542 * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
   543   Refined theory on complete lattices.
   544 
   545 * August 2011: Brian Huffman, Portland State University
   546   Miscellaneous cleanup of Complex_Main and Multivariate_Analysis.
   547 
   548 * June 2011: Brian Huffman, Portland State University
   549   Proof method "countable_datatype" for theory Library/Countable.
   550 
   551 * 2011: Jasmin Blanchette, TUM
   552   Various improvements to Sledgehammer, notably: use of sound
   553   translations, support for more provers (Waldmeister, LEO-II,
   554   Satallax). Further development of Nitpick and 'try' command.
   555 
   556 * 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
   557   Theory HOL/Library/Cset_Monad allows do notation for computable sets
   558   (cset) via the generic monad ad-hoc overloading facility.
   559 
   560 * 2011: Johannes Hölzl, Armin Heller, TUM and
   561   Bogdan Grechuk, University of Edinburgh
   562   Theory HOL/Library/Extended_Reals: real numbers extended with plus
   563   and minus infinity.
   564 
   565 * 2011: Makarius Wenzel, Université Paris-Sud / LRI
   566   Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
   567   Prover IDE.
   568 
   569 
   570 Contributions to Isabelle2011
   571 -----------------------------
   572 
   573 * January 2011: Stefan Berghofer, secunet Security Networks AG
   574   HOL-SPARK: an interactive prover back-end for SPARK.
   575 
   576 * October 2010: Bogdan Grechuk, University of Edinburgh
   577   Extended convex analysis in Multivariate Analysis.
   578 
   579 * October 2010: Dmitriy Traytel, TUM
   580   Coercive subtyping via subtype constraints.
   581 
   582 * October 2010: Alexander Krauss, TUM
   583   Command partial_function for function definitions based on complete
   584   partial orders in HOL.
   585 
   586 * September 2010: Florian Haftmann, TUM
   587   Refined concepts for evaluation, i.e., normalization of terms using
   588   different techniques.
   589 
   590 * September 2010: Florian Haftmann, TUM
   591   Code generation for Scala.
   592 
   593 * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
   594   Improved Probability theory in HOL.
   595 
   596 * July 2010: Florian Haftmann, TUM
   597   Reworking and extension of the Imperative HOL framework.
   598 
   599 * July 2010: Alexander Krauss, TUM and Christian Sternagel, University
   600     of Innsbruck
   601   Ad-hoc overloading. Generic do notation for monads.
   602 
   603 
   604 Contributions to Isabelle2009-2
   605 -------------------------------
   606 
   607 * 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM,
   608   Makarius Wenzel, TUM / LRI
   609   Elimination of type classes from proof terms.
   610 
   611 * April 2010: Florian Haftmann, TUM
   612   Reorganization of abstract algebra type classes.
   613 
   614 * April 2010: Florian Haftmann, TUM
   615   Code generation for data representations involving invariants;
   616   various collections avaiable in theories Fset, Dlist, RBT,
   617   Mapping and AssocList.
   618 
   619 * March 2010: Sascha Boehme, TUM
   620   Efficient SHA1 library for Poly/ML.
   621 
   622 * February 2010: Cezary Kaliszyk and Christian Urban, TUM
   623   Quotient type package for Isabelle/HOL.
   624 
   625 
   626 Contributions to Isabelle2009-1
   627 -------------------------------
   628 
   629 * November 2009, Brian Huffman, PSU
   630   New definitional domain package for HOLCF.
   631 
   632 * November 2009: Robert Himmelmann, TUM
   633   Derivation and Brouwer's fixpoint theorem in Multivariate Analysis.
   634 
   635 * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM
   636   A tabled implementation of the reflexive transitive closure.
   637 
   638 * November 2009: Lukas Bulwahn, TUM
   639   Predicate Compiler: a compiler for inductive predicates to
   640   equational specifications.
   641 
   642 * November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris
   643   HOL-Boogie: an interactive prover back-end for Boogie and VCC.
   644 
   645 * October 2009: Jasmin Blanchette, TUM
   646   Nitpick: yet another counterexample generator for Isabelle/HOL.
   647 
   648 * October 2009: Sascha Boehme, TUM
   649   Extension of SMT method: proof-reconstruction for the SMT solver Z3.
   650 
   651 * October 2009: Florian Haftmann, TUM
   652   Refinement of parts of the HOL datatype package.
   653 
   654 * October 2009: Florian Haftmann, TUM
   655   Generic term styles for term antiquotations.
   656 
   657 * September 2009: Thomas Sewell, NICTA
   658   More efficient HOL/record implementation.
   659 
   660 * September 2009: Sascha Boehme, TUM
   661   SMT method using external SMT solvers.
   662 
   663 * September 2009: Florian Haftmann, TUM
   664   Refinement of sets and lattices.
   665 
   666 * July 2009: Jeremy Avigad and Amine Chaieb
   667   New number theory.
   668 
   669 * July 2009: Philipp Meyer, TUM
   670   HOL/Library/Sum_Of_Squares: functionality to call a remote csdp
   671   prover.
   672 
   673 * July 2009: Florian Haftmann, TUM
   674   New quickcheck implementation using new code generator.
   675 
   676 * July 2009: Florian Haftmann, TUM
   677   HOL/Library/Fset: an explicit type of sets; finite sets ready to use
   678   for code generation.
   679 
   680 * June 2009: Florian Haftmann, TUM
   681   HOL/Library/Tree: search trees implementing mappings, ready to use
   682   for code generation.
   683 
   684 * March 2009: Philipp Meyer, TUM
   685   Minimization tool for results from Sledgehammer.
   686 
   687 
   688 Contributions to Isabelle2009
   689 -----------------------------
   690 
   691 * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
   692   Cambridge
   693   Elementary topology in Euclidean space.
   694 
   695 * March 2009: Johannes Hoelzl, TUM
   696   Method "approximation", which proves real valued inequalities by
   697   computation.
   698 
   699 * February 2009: Filip Maric, Univ. of Belgrade
   700   A Serbian theory.
   701 
   702 * February 2009: Jasmin Christian Blanchette, TUM
   703   Misc cleanup of HOL/refute.
   704 
   705 * February 2009: Timothy Bourke, NICTA
   706   New find_consts command.
   707 
   708 * February 2009: Timothy Bourke, NICTA
   709   "solves" criterion for find_theorems and auto_solve option
   710 
   711 * December 2008: Clemens Ballarin, TUM
   712   New locale implementation.
   713 
   714 * December 2008: Armin Heller, TUM and Alexander Krauss, TUM
   715   Method "sizechange" for advanced termination proofs.
   716 
   717 * November 2008: Timothy Bourke, NICTA
   718   Performance improvement (factor 50) for find_theorems.
   719 
   720 * 2008: Florian Haftmann, TUM
   721   Various extensions and restructurings in HOL, improvements
   722   in evaluation mechanisms, new module binding.ML for name bindings.
   723 
   724 * October 2008: Fabian Immler, TUM
   725   ATP manager for Sledgehammer, based on ML threads instead of Posix
   726   processes.  Additional ATP wrappers, including remote SystemOnTPTP
   727   services.
   728 
   729 * September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen
   730   Prover for coherent logic.
   731 
   732 * August 2008: Fabian Immler, TUM
   733   Vampire wrapper script for remote SystemOnTPTP service.
   734 
   735 
   736 Contributions to Isabelle2008
   737 -----------------------------
   738 
   739 * 2007/2008:
   740   Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM
   741   HOL library improvements.
   742 
   743 * 2007/2008: Brian Huffman, PSU
   744   HOLCF library improvements.
   745 
   746 * 2007/2008: Stefan Berghofer, TUM
   747   HOL-Nominal package improvements.
   748 
   749 * March 2008: Markus Reiter, TUM
   750   HOL/Library/RBT: red-black trees.
   751 
   752 * February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and
   753   Lukas Bulwahn, TUM and John Matthews, Galois:
   754   HOL/Library/Imperative_HOL: Haskell-style imperative data structures
   755   for HOL.
   756 
   757 * December 2007: Norbert Schirmer, Uni Saarbruecken
   758   Misc improvements of record package in HOL.
   759 
   760 * December 2007: Florian Haftmann, TUM
   761   Overloading and class instantiation target.
   762 
   763 * December 2007: Florian Haftmann, TUM
   764   New version of primrec package for local theories.
   765 
   766 * December 2007: Alexander Krauss, TUM
   767   Method "induction_scheme" in HOL.
   768 
   769 * November 2007: Peter Lammich, Uni Muenster
   770   HOL-Lattice: some more lemmas.
   771 
   772 
   773 Contributions to Isabelle2007
   774 -----------------------------
   775 
   776 * October 2007: Norbert Schirmer, TUM / Uni Saarbruecken
   777   State Spaces: The Locale Way (in HOL).
   778 
   779 * October 2007: Mark A. Hillebrand, DFKI
   780   Robust sub/superscripts in LaTeX document output.
   781 
   782 * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian
   783     Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois
   784   HOL-Word: a library for fixed-size machine words in Isabelle.
   785 
   786 * August 2007: Brian Huffman, PSU
   787   HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type.
   788 
   789 * June 2007: Amine Chaieb, TUM
   790   Semiring normalization and Groebner Bases.
   791   Support for dense linear orders.
   792 
   793 * June 2007: Joe Hurd, Oxford
   794   Metis theorem-prover.
   795 
   796 * 2007: Kong W. Susanto, Cambridge
   797   HOL: Metis prover integration.
   798 
   799 * 2007: Stefan Berghofer, TUM
   800   HOL: inductive predicates and sets.
   801 
   802 * 2007: Norbert Schirmer, TUM
   803   HOL/record: misc improvements.
   804 
   805 * 2006/2007: Alexander Krauss, TUM
   806   HOL: function package and related theories on termination.
   807 
   808 * 2006/2007: Florian Haftmann, TUM
   809   Pure: generic code generator framework.
   810   Pure: class package.
   811   HOL: theory reorganization, code generator setup.
   812 
   813 * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and
   814     Julien Narboux, TUM
   815   HOL/Nominal package and related tools.
   816 
   817 * November 2006: Lukas Bulwahn, TUM
   818   HOL: method "lexicographic_order" for function package.
   819 
   820 * October 2006: Stefan Hohe, TUM
   821   HOL-Algebra: ideals and quotients over rings.
   822 
   823 * August 2006: Amine Chaieb, TUM
   824   Experimental support for generic reflection and reification in HOL.
   825 
   826 * July 2006: Rafal Kolanski, NICTA
   827   Hex (0xFF) and binary (0b1011) numerals.
   828 
   829 * May 2006: Klaus Aehlig, LMU
   830   Command 'normal_form': normalization by evaluation.
   831 
   832 * May 2006: Amine Chaieb, TUM
   833   HOL-Complex: Ferrante and Rackoff Algorithm for linear real
   834   arithmetic.
   835 
   836 * February 2006: Benjamin Porter, NICTA
   837   HOL and HOL-Complex: generalised mean value theorem, continuum is
   838   not denumerable, harmonic and arithmetic series, and denumerability
   839   of rationals.
   840 
   841 * October 2005: Martin Wildmoser, TUM
   842   Sketch for Isar 'guess' element.
   843 
   844 
   845 Contributions to Isabelle2005
   846 -----------------------------
   847 
   848 * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
   849   HOL-Complex: Formalization of Taylor series.
   850 
   851 * September 2005: Stephan Merz, Alwen Tiu, QSL Loria
   852   Components for SAT solver method using zChaff.
   853 
   854 * September 2005: Ning Zhang and Christian Urban, LMU Munich
   855   A Chinese theory.
   856 
   857 * September 2005: Bernhard Haeupler, TUM
   858   Method comm_ring for proving equalities in commutative rings.
   859 
   860 * July/August 2005: Jeremy Avigad, Carnegie Mellon University
   861   Various improvements of the HOL and HOL-Complex library.
   862 
   863 * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
   864   Some structured proofs about completeness of real numbers.
   865 
   866 * May 2005: Rafal Kolanski and Gerwin Klein, NICTA
   867   Improved retrieval of facts from theory/proof context.
   868 
   869 * February 2005: Lucas Dixon, University of Edinburgh
   870   Improved subst method.
   871 
   872 * 2005: Brian Huffman, OGI
   873   Various improvements of HOLCF.
   874   Some improvements of the HOL-Complex library.
   875 
   876 * 2005: Claire Quigley and Jia Meng, University of Cambridge
   877   Some support for asynchronous communication with external provers
   878   (experimental).
   879 
   880 * 2005: Florian Haftmann, TUM
   881   Contributions to document 'sugar'.
   882   Various ML combinators, notably linear functional transformations.
   883   Some cleanup of ML legacy.
   884   Additional antiquotations.
   885   Improved Isabelle web site.
   886 
   887 * 2004/2005: David Aspinall, University of Edinburgh
   888   Various elements of XML and PGIP based communication with user
   889   interfaces (experimental).
   890 
   891 * 2004/2005: Gerwin Klein, NICTA
   892   Contributions to document 'sugar'.
   893   Improved Isabelle web site.
   894   Improved HTML presentation of theories.
   895 
   896 * 2004/2005: Clemens Ballarin, TUM
   897   Provers: tools for transitive relations and quasi orders.
   898   Improved version of locales, notably interpretation of locales.
   899   Improved version of HOL-Algebra.
   900 
   901 * 2004/2005: Amine Chaieb, TUM
   902   Improved version of HOL presburger method.
   903 
   904 * 2004/2005: Steven Obua, TUM
   905   Improved version of HOL/Import, support for HOL-Light.
   906   Improved version of HOL-Complex-Matrix.
   907   Pure/defs: more sophisticated checks on well-formedness of overloading.
   908   Pure/Tools: an experimental evaluator for lambda terms.
   909 
   910 * 2004/2005: Norbert Schirmer, TUM
   911   Contributions to document 'sugar'.
   912   Improved version of HOL/record.
   913 
   914 * 2004/2005: Sebastian Skalberg, TUM
   915   Improved version of HOL/Import.
   916   Some internal ML reorganizations.
   917 
   918 * 2004/2005: Tjark Weber, TUM
   919   SAT solver method using zChaff.
   920   Improved version of HOL/refute.
   921 
   922 :maxLineLen=78: