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