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