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