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