CONTRIBUTORS
author kuncar
Thu May 24 14:20:23 2012 +0200 (2012-05-24)
changeset 47982 7aa35601ff65
parent 47887 4e9c06c194d9
child 48111 33414f2e82ab
permissions -rw-r--r--
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
     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
     3 who is listed as an author in one of the source files of this Isabelle
     4 distribution.
     5 
     6 Contributions to this Isabelle version
     7 --------------------------------------
     8 
     9 
    10 Contributions to Isabelle2012
    11 -----------------------------
    12 
    13 * April 2012: Johannes Hölzl, TUM
    14   Probability: Introduced type to represent measures instead of
    15   locales.
    16 
    17 * April 2012: Johannes Hölzl, Fabian Immler, TUM
    18   Float: Moved to Dyadic rationals to represent floating point numers.
    19 
    20 * April 2012: Thomas Sewell, NICTA and
    21   2010: Sascha Boehme, TUM
    22   Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector
    23   equalities/inequalities.
    24 
    25 * March 2012: Christian Sternagel, JAIST
    26   Consolidated theory of relation composition.
    27 
    28 * March 2012: Nik Sultana, University of Cambridge
    29   HOL/TPTP parser and import facilities.
    30 
    31 * March 2012: Cezary Kaliszyk, University of Innsbruck and
    32   Alexander Krauss, QAware GmbH
    33   Faster and more scalable Import mechanism for HOL Light proofs.
    34 
    35 * January 2012: Florian Haftmann, TUM, et al.
    36   (Re-)Introduction of the "set" type constructor.
    37 
    38 * 2012: Ondrej Kuncar, TUM
    39   New package Lifting, various improvements and refinements to the
    40   Quotient package.
    41 
    42 * 2011/2012: Jasmin Blanchette, TUM
    43   Various improvements to Sledgehammer, notably: tighter integration
    44   with SPASS, support for more provers (Alt-Ergo, iProver,
    45   iProver-Eq).
    46 
    47 * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI
    48   Various refinements of local theory infrastructure.
    49   Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE.
    50 
    51 
    52 Contributions to Isabelle2011-1
    53 -------------------------------
    54 
    55 * September 2011: Peter Gammie
    56   Theory HOL/Library/Saturated: numbers with saturated arithmetic.
    57 
    58 * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
    59   Refined theory on complete lattices.
    60 
    61 * August 2011: Brian Huffman, Portland State University
    62   Miscellaneous cleanup of Complex_Main and Multivariate_Analysis.
    63 
    64 * June 2011: Brian Huffman, Portland State University
    65   Proof method "countable_datatype" for theory Library/Countable.
    66 
    67 * 2011: Jasmin Blanchette, TUM
    68   Various improvements to Sledgehammer, notably: use of sound
    69   translations, support for more provers (Waldmeister, LEO-II,
    70   Satallax). Further development of Nitpick and 'try' command.
    71 
    72 * 2011: Andreas Lochbihler, Karlsruhe Institute of Technology
    73   Theory HOL/Library/Cset_Monad allows do notation for computable sets
    74   (cset) via the generic monad ad-hoc overloading facility.
    75 
    76 * 2011: Johannes Hölzl, Armin Heller, TUM and
    77   Bogdan Grechuk, University of Edinburgh
    78   Theory HOL/Library/Extended_Reals: real numbers extended with plus
    79   and minus infinity.
    80 
    81 * 2011: Makarius Wenzel, Université Paris-Sud / LRI
    82   Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
    83   Prover IDE.
    84 
    85 
    86 Contributions to Isabelle2011
    87 -----------------------------
    88 
    89 * January 2011: Stefan Berghofer, secunet Security Networks AG
    90   HOL-SPARK: an interactive prover back-end for SPARK.
    91 
    92 * October 2010: Bogdan Grechuk, University of Edinburgh
    93   Extended convex analysis in Multivariate Analysis.
    94 
    95 * October 2010: Dmitriy Traytel, TUM
    96   Coercive subtyping via subtype constraints.
    97 
    98 * October 2010: Alexander Krauss, TUM
    99   Command partial_function for function definitions based on complete
   100   partial orders in HOL.
   101 
   102 * September 2010: Florian Haftmann, TUM
   103   Refined concepts for evaluation, i.e., normalization of terms using
   104   different techniques.
   105 
   106 * September 2010: Florian Haftmann, TUM
   107   Code generation for Scala.
   108 
   109 * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
   110   Improved Probability theory in HOL.
   111 
   112 * July 2010: Florian Haftmann, TUM
   113   Reworking and extension of the Imperative HOL framework.
   114 
   115 * July 2010: Alexander Krauss, TUM and Christian Sternagel, University
   116     of Innsbruck
   117   Ad-hoc overloading. Generic do notation for monads.
   118 
   119 
   120 Contributions to Isabelle2009-2
   121 -------------------------------
   122 
   123 * 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM,
   124   Makarius Wenzel, TUM / LRI
   125   Elimination of type classes from proof terms.
   126 
   127 * April 2010: Florian Haftmann, TUM
   128   Reorganization of abstract algebra type classes.
   129 
   130 * April 2010: Florian Haftmann, TUM
   131   Code generation for data representations involving invariants;
   132   various collections avaiable in theories Fset, Dlist, RBT,
   133   Mapping and AssocList.
   134 
   135 * March 2010: Sascha Boehme, TUM
   136   Efficient SHA1 library for Poly/ML.
   137 
   138 * February 2010: Cezary Kaliszyk and Christian Urban, TUM
   139   Quotient type package for Isabelle/HOL.
   140 
   141 
   142 Contributions to Isabelle2009-1
   143 -------------------------------
   144 
   145 * November 2009, Brian Huffman, PSU
   146   New definitional domain package for HOLCF.
   147 
   148 * November 2009: Robert Himmelmann, TUM
   149   Derivation and Brouwer's fixpoint theorem in Multivariate Analysis.
   150 
   151 * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM
   152   A tabled implementation of the reflexive transitive closure.
   153 
   154 * November 2009: Lukas Bulwahn, TUM
   155   Predicate Compiler: a compiler for inductive predicates to
   156   equational specifications.
   157  
   158 * November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris
   159   HOL-Boogie: an interactive prover back-end for Boogie and VCC.
   160 
   161 * October 2009: Jasmin Blanchette, TUM
   162   Nitpick: yet another counterexample generator for Isabelle/HOL.
   163 
   164 * October 2009: Sascha Boehme, TUM
   165   Extension of SMT method: proof-reconstruction for the SMT solver Z3.
   166 
   167 * October 2009: Florian Haftmann, TUM
   168   Refinement of parts of the HOL datatype package.
   169 
   170 * October 2009: Florian Haftmann, TUM
   171   Generic term styles for term antiquotations.
   172 
   173 * September 2009: Thomas Sewell, NICTA
   174   More efficient HOL/record implementation.
   175 
   176 * September 2009: Sascha Boehme, TUM
   177   SMT method using external SMT solvers.
   178 
   179 * September 2009: Florian Haftmann, TUM
   180   Refinement of sets and lattices.
   181 
   182 * July 2009: Jeremy Avigad and Amine Chaieb
   183   New number theory.
   184 
   185 * July 2009: Philipp Meyer, TUM
   186   HOL/Library/Sum_Of_Squares: functionality to call a remote csdp
   187   prover.
   188 
   189 * July 2009: Florian Haftmann, TUM
   190   New quickcheck implementation using new code generator.
   191 
   192 * July 2009: Florian Haftmann, TUM
   193   HOL/Library/Fset: an explicit type of sets; finite sets ready to use
   194   for code generation.
   195 
   196 * June 2009: Florian Haftmann, TUM
   197   HOL/Library/Tree: search trees implementing mappings, ready to use
   198   for code generation.
   199 
   200 * March 2009: Philipp Meyer, TUM
   201   Minimization tool for results from Sledgehammer.
   202 
   203 
   204 Contributions to Isabelle2009
   205 -----------------------------
   206 
   207 * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
   208   Cambridge
   209   Elementary topology in Euclidean space.
   210 
   211 * March 2009: Johannes Hoelzl, TUM
   212   Method "approximation", which proves real valued inequalities by
   213   computation.
   214 
   215 * February 2009: Filip Maric, Univ. of Belgrade
   216   A Serbian theory.
   217 
   218 * February 2009: Jasmin Christian Blanchette, TUM
   219   Misc cleanup of HOL/refute.
   220 
   221 * February 2009: Timothy Bourke, NICTA
   222   New find_consts command.
   223 
   224 * February 2009: Timothy Bourke, NICTA
   225   "solves" criterion for find_theorems and auto_solve option
   226 
   227 * December 2008: Clemens Ballarin, TUM
   228   New locale implementation.
   229 
   230 * December 2008: Armin Heller, TUM and Alexander Krauss, TUM
   231   Method "sizechange" for advanced termination proofs.
   232 
   233 * November 2008: Timothy Bourke, NICTA
   234   Performance improvement (factor 50) for find_theorems.
   235 
   236 * 2008: Florian Haftmann, TUM
   237   Various extensions and restructurings in HOL, improvements
   238   in evaluation mechanisms, new module binding.ML for name bindings.
   239 
   240 * October 2008: Fabian Immler, TUM
   241   ATP manager for Sledgehammer, based on ML threads instead of Posix
   242   processes.  Additional ATP wrappers, including remote SystemOnTPTP
   243   services.
   244 
   245 * September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen
   246   Prover for coherent logic.
   247 
   248 * August 2008: Fabian Immler, TUM
   249   Vampire wrapper script for remote SystemOnTPTP service.
   250 
   251 
   252 Contributions to Isabelle2008
   253 -----------------------------
   254 
   255 * 2007/2008:
   256   Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM
   257   HOL library improvements.
   258 
   259 * 2007/2008: Brian Huffman, PSU
   260   HOLCF library improvements.
   261 
   262 * 2007/2008: Stefan Berghofer, TUM
   263   HOL-Nominal package improvements.
   264 
   265 * March 2008: Markus Reiter, TUM
   266   HOL/Library/RBT: red-black trees.
   267 
   268 * February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and
   269   Lukas Bulwahn, TUM and John Matthews, Galois:
   270   HOL/Library/Imperative_HOL: Haskell-style imperative data structures
   271   for HOL.
   272 
   273 * December 2007: Norbert Schirmer, Uni Saarbruecken
   274   Misc improvements of record package in HOL.
   275 
   276 * December 2007: Florian Haftmann, TUM
   277   Overloading and class instantiation target.
   278 
   279 * December 2007: Florian Haftmann, TUM
   280   New version of primrec package for local theories.
   281 
   282 * December 2007: Alexander Krauss, TUM
   283   Method "induction_scheme" in HOL.
   284 
   285 * November 2007: Peter Lammich, Uni Muenster
   286   HOL-Lattice: some more lemmas.
   287 
   288 
   289 Contributions to Isabelle2007
   290 -----------------------------
   291 
   292 * October 2007: Norbert Schirmer, TUM / Uni Saarbruecken
   293   State Spaces: The Locale Way (in HOL).
   294 
   295 * October 2007: Mark A. Hillebrand, DFKI
   296   Robust sub/superscripts in LaTeX document output.
   297 
   298 * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian
   299     Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois
   300   HOL-Word: a library for fixed-size machine words in Isabelle.
   301 
   302 * August 2007: Brian Huffman, PSU
   303   HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type.
   304 
   305 * June 2007: Amine Chaieb, TUM
   306   Semiring normalization and Groebner Bases.
   307   Support for dense linear orders.
   308 
   309 * June 2007: Joe Hurd, Oxford
   310   Metis theorem-prover.
   311 
   312 * 2007: Kong W. Susanto, Cambridge
   313   HOL: Metis prover integration.
   314 
   315 * 2007: Stefan Berghofer, TUM
   316   HOL: inductive predicates and sets.
   317 
   318 * 2007: Norbert Schirmer, TUM
   319   HOL/record: misc improvements.
   320 
   321 * 2006/2007: Alexander Krauss, TUM
   322   HOL: function package and related theories on termination.
   323 
   324 * 2006/2007: Florian Haftmann, TUM
   325   Pure: generic code generator framework.
   326   Pure: class package.
   327   HOL: theory reorganization, code generator setup.
   328 
   329 * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and
   330     Julien Narboux, TUM
   331   HOL/Nominal package and related tools.
   332 
   333 * November 2006: Lukas Bulwahn, TUM
   334   HOL: method "lexicographic_order" for function package.
   335 
   336 * October 2006: Stefan Hohe, TUM
   337   HOL-Algebra: ideals and quotients over rings.
   338 
   339 * August 2006: Amine Chaieb, TUM
   340   Experimental support for generic reflection and reification in HOL.
   341 
   342 * July 2006: Rafal Kolanski, NICTA
   343   Hex (0xFF) and binary (0b1011) numerals.
   344 
   345 * May 2006: Klaus Aehlig, LMU
   346   Command 'normal_form': normalization by evaluation.
   347 
   348 * May 2006: Amine Chaieb, TUM
   349   HOL-Complex: Ferrante and Rackoff Algorithm for linear real
   350   arithmetic.
   351 
   352 * February 2006: Benjamin Porter, NICTA
   353   HOL and HOL-Complex: generalised mean value theorem, continuum is
   354   not denumerable, harmonic and arithmetic series, and denumerability
   355   of rationals.
   356 
   357 * October 2005: Martin Wildmoser, TUM
   358   Sketch for Isar 'guess' element.
   359 
   360 
   361 Contributions to Isabelle2005
   362 -----------------------------
   363 
   364 * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
   365   HOL-Complex: Formalization of Taylor series.
   366 
   367 * September 2005: Stephan Merz, Alwen Tiu, QSL Loria
   368   Components for SAT solver method using zChaff.
   369 
   370 * September 2005: Ning Zhang and Christian Urban, LMU Munich
   371   A Chinese theory.
   372 
   373 * September 2005: Bernhard Haeupler, TUM
   374   Method comm_ring for proving equalities in commutative rings.
   375 
   376 * July/August 2005: Jeremy Avigad, Carnegie Mellon University
   377   Various improvements of the HOL and HOL-Complex library.
   378 
   379 * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
   380   Some structured proofs about completeness of real numbers.
   381 
   382 * May 2005: Rafal Kolanski and Gerwin Klein, NICTA
   383   Improved retrieval of facts from theory/proof context.
   384 
   385 * February 2005: Lucas Dixon, University of Edinburgh
   386   Improved subst method.
   387 
   388 * 2005: Brian Huffman, OGI
   389   Various improvements of HOLCF.
   390   Some improvements of the HOL-Complex library.
   391 
   392 * 2005: Claire Quigley and Jia Meng, University of Cambridge
   393   Some support for asynchronous communication with external provers
   394   (experimental).
   395 
   396 * 2005: Florian Haftmann, TUM
   397   Contributions to document 'sugar'.
   398   Various ML combinators, notably linear functional transformations.
   399   Some cleanup of ML legacy.
   400   Additional antiquotations.
   401   Improved Isabelle web site.
   402 
   403 * 2004/2005: David Aspinall, University of Edinburgh
   404   Various elements of XML and PGIP based communication with user
   405   interfaces (experimental).
   406 
   407 * 2004/2005: Gerwin Klein, NICTA
   408   Contributions to document 'sugar'.
   409   Improved Isabelle web site.
   410   Improved HTML presentation of theories.
   411 
   412 * 2004/2005: Clemens Ballarin, TUM
   413   Provers: tools for transitive relations and quasi orders.
   414   Improved version of locales, notably interpretation of locales.
   415   Improved version of HOL-Algebra.
   416 
   417 * 2004/2005: Amine Chaieb, TUM
   418   Improved version of HOL presburger method.
   419 
   420 * 2004/2005: Steven Obua, TUM
   421   Improved version of HOL/Import, support for HOL-Light.
   422   Improved version of HOL-Complex-Matrix.
   423   Pure/defs: more sophisticated checks on well-formedness of overloading.
   424   Pure/Tools: an experimental evaluator for lambda terms.
   425 
   426 * 2004/2005: Norbert Schirmer, TUM
   427   Contributions to document 'sugar'.
   428   Improved version of HOL/record.
   429 
   430 * 2004/2005: Sebastian Skalberg, TUM
   431   Improved version of HOL/Import.
   432   Some internal ML reorganizations.
   433 
   434 * 2004/2005: Tjark Weber, TUM
   435   SAT solver method using zChaff.
   436   Improved version of HOL/refute.