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