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