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