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