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