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