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