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