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