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