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