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