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