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