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