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