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