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