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