CONTRIBUTORS
author hoelzl
Mon Aug 23 19:35:57 2010 +0200 (2010-08-23)
changeset 38656 d5d342611edb
parent 38461 75fc4087764e
child 39644 ad436fa9fc5b
permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
wenzelm@24799
     1
For the purposes of the license agreement in the file COPYRIGHT, a
wenzelm@24799
     2
'contributor' is anybody who is listed in this file (CONTRIBUTORS) or
kleing@23382
     3
who is listed as an author in one of the source files of this Isabelle
kleing@23382
     4
distribution.
kleing@23382
     5
wenzelm@37383
     6
Contributions to this Isabelle version
wenzelm@37383
     7
--------------------------------------
wenzelm@37383
     8
hoelzl@38656
     9
* August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
hoelzl@38656
    10
  Rewriting the Probability theory.
hoelzl@38656
    11
haftmann@38461
    12
* July 2010: Florian Haftmann, TUM
haftmann@38461
    13
  Reworking and extension of the Isabelle/HOL framework.
haftmann@38461
    14
wenzelm@37383
    15
wenzelm@37144
    16
Contributions to Isabelle2009-2
wenzelm@33951
    17
--------------------------------------
wenzelm@33951
    18
krauss@37303
    19
* 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM,
krauss@37303
    20
  Makarius Wenzel, TUM / LRI
krauss@37303
    21
  Elimination of type classes from proof terms.
krauss@37303
    22
wenzelm@37144
    23
* April 2010: Florian Haftmann, TUM
haftmann@36416
    24
  Reorganization of abstract algebra type classes.
haftmann@36416
    25
wenzelm@37144
    26
* April 2010: Florian Haftmann, TUM
haftmann@36416
    27
  Code generation for data representations involving invariants;
haftmann@36416
    28
  various collections avaiable in theories Fset, Dlist, RBT,
haftmann@36416
    29
  Mapping and AssocList.
haftmann@36416
    30
wenzelm@37144
    31
* March 2010: Sascha Boehme, TUM
wenzelm@37144
    32
  Efficient SHA1 library for Poly/ML.
wenzelm@37144
    33
wenzelm@37282
    34
* February 2010: Cezary Kaliszyk and Christian Urban, TUM
wenzelm@37282
    35
  Quotient type package for Isabelle/HOL.
wenzelm@37282
    36
wenzelm@26874
    37
wenzelm@33842
    38
Contributions to Isabelle2009-1
wenzelm@33842
    39
-------------------------------
bulwahn@33649
    40
haftmann@33862
    41
* November 2009, Brian Huffman, PSU
haftmann@33862
    42
  New definitional domain package for HOLCF.
haftmann@33862
    43
hoelzl@33759
    44
* November 2009: Robert Himmelmann, TUM
haftmann@33862
    45
  Derivation and Brouwer's fixpoint theorem in Multivariate Analysis.
hoelzl@33759
    46
wenzelm@33842
    47
* November 2009: Stefan Berghofer and Lukas Bulwahn, TUM
wenzelm@33842
    48
  A tabled implementation of the reflexive transitive closure.
bulwahn@33649
    49
bulwahn@33627
    50
* November 2009: Lukas Bulwahn, TUM
wenzelm@33842
    51
  Predicate Compiler: a compiler for inductive predicates to
wenzelm@33843
    52
  equational specifications.
bulwahn@33627
    53
 
wenzelm@33897
    54
* November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris
wenzelm@33842
    55
  HOL-Boogie: an interactive prover back-end for Boogie and VCC.
boehmes@33419
    56
blanchet@33192
    57
* October 2009: Jasmin Blanchette, TUM
wenzelm@33842
    58
  Nitpick: yet another counterexample generator for Isabelle/HOL.
blanchet@33192
    59
boehmes@33010
    60
* October 2009: Sascha Boehme, TUM
wenzelm@33182
    61
  Extension of SMT method: proof-reconstruction for the SMT solver Z3.
boehmes@33010
    62
boehmes@33010
    63
* October 2009: Florian Haftmann, TUM
wenzelm@33182
    64
  Refinement of parts of the HOL datatype package.
haftmann@33005
    65
boehmes@33010
    66
* October 2009: Florian Haftmann, TUM
wenzelm@33182
    67
  Generic term styles for term antiquotations.
haftmann@33005
    68
wenzelm@32762
    69
* September 2009: Thomas Sewell, NICTA
wenzelm@33182
    70
  More efficient HOL/record implementation.
wenzelm@32762
    71
boehmes@32618
    72
* September 2009: Sascha Boehme, TUM
wenzelm@33182
    73
  SMT method using external SMT solvers.
boehmes@32618
    74
haftmann@32600
    75
* September 2009: Florian Haftmann, TUM
wenzelm@33182
    76
  Refinement of sets and lattices.
haftmann@32600
    77
haftmann@32600
    78
* July 2009: Jeremy Avigad and Amine Chaieb
wenzelm@33182
    79
  New number theory.
haftmann@32600
    80
Philipp@32268
    81
* July 2009: Philipp Meyer, TUM
wenzelm@33182
    82
  HOL/Library/Sum_Of_Squares: functionality to call a remote csdp
wenzelm@33182
    83
  prover.
Philipp@32268
    84
haftmann@31997
    85
* July 2009: Florian Haftmann, TUM
wenzelm@33182
    86
  New quickcheck implementation using new code generator.
haftmann@31997
    87
haftmann@31997
    88
* July 2009: Florian Haftmann, TUM
wenzelm@33182
    89
  HOL/Library/FSet: an explicit type of sets; finite sets ready to use
wenzelm@33182
    90
  for code generation.
haftmann@31466
    91
haftmann@31466
    92
* June 2009: Florian Haftmann, TUM
wenzelm@33843
    93
  HOL/Library/Tree: search trees implementing mappings, ready to use
wenzelm@33182
    94
  for code generation.
wenzelm@30978
    95
Philipp@32268
    96
* March 2009: Philipp Meyer, TUM
wenzelm@33843
    97
  Minimization tool for results from Sledgehammer.
wenzelm@33182
    98
Philipp@32268
    99
wenzelm@30978
   100
Contributions to Isabelle2009
wenzelm@30978
   101
-----------------------------
wenzelm@30978
   102
wenzelm@30383
   103
* March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
wenzelm@30383
   104
  Cambridge
wenzelm@30383
   105
  Elementary topology in Euclidean space.
wenzelm@30383
   106
wenzelm@30886
   107
* March 2009: Johannes Hoelzl, TUM
wenzelm@30886
   108
  Method "approximation", which proves real valued inequalities by
wenzelm@30886
   109
  computation.
wenzelm@30886
   110
wenzelm@30179
   111
* February 2009: Filip Maric, Univ. of Belgrade
wenzelm@30179
   112
  A Serbian theory.
wenzelm@30179
   113
wenzelm@30162
   114
* February 2009: Jasmin Christian Blanchette, TUM
wenzelm@30154
   115
  Misc cleanup of HOL/refute.
wenzelm@30154
   116
wenzelm@30162
   117
* February 2009: Timothy Bourke, NICTA
kleing@29883
   118
  New find_consts command.
kleing@29883
   119
wenzelm@30162
   120
* February 2009: Timothy Bourke, NICTA
kleing@29861
   121
  "solves" criterion for find_theorems and auto_solve option
kleing@29861
   122
haftmann@29398
   123
* December 2008: Clemens Ballarin, TUM
haftmann@29398
   124
  New locale implementation.
haftmann@29398
   125
krauss@29182
   126
* December 2008: Armin Heller, TUM and Alexander Krauss, TUM
krauss@29182
   127
  Method "sizechange" for advanced termination proofs.
krauss@29182
   128
kleing@28901
   129
* November 2008: Timothy Bourke, NICTA
kleing@28901
   130
  Performance improvement (factor 50) for find_theorems.
kleing@28901
   131
haftmann@29398
   132
* 2008: Florian Haftmann, TUM
haftmann@29398
   133
  Various extensions and restructurings in HOL, improvements
haftmann@29398
   134
  in evaluation mechanisms, new module binding.ML for name bindings.
haftmann@29398
   135
wenzelm@28604
   136
* October 2008: Fabian Immler, TUM
wenzelm@28604
   137
  ATP manager for Sledgehammer, based on ML threads instead of Posix
wenzelm@28604
   138
  processes.  Additional ATP wrappers, including remote SystemOnTPTP
wenzelm@28604
   139
  services.
wenzelm@28604
   140
wenzelm@30162
   141
* September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen
wenzelm@30162
   142
  Prover for coherent logic.
wenzelm@30162
   143
wenzelm@28474
   144
* August 2008: Fabian Immler, TUM
wenzelm@28474
   145
  Vampire wrapper script for remote SystemOnTPTP service.
wenzelm@28474
   146
wenzelm@28474
   147
wenzelm@28474
   148
Contributions to Isabelle2008
wenzelm@28474
   149
-----------------------------
wenzelm@28474
   150
wenzelm@27009
   151
* 2007/2008:
wenzelm@27009
   152
  Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM
wenzelm@27009
   153
  HOL library improvements.
wenzelm@25468
   154
wenzelm@27009
   155
* 2007/2008: Brian Huffman, PSU
wenzelm@27009
   156
  HOLCF library improvements.
wenzelm@27009
   157
wenzelm@27009
   158
* 2007/2008: Stefan Berghofer, TUM
wenzelm@30179
   159
  HOL-Nominal package improvements.
wenzelm@27009
   160
wenzelm@27009
   161
* March 2008: Markus Reiter, TUM
wenzelm@27009
   162
  HOL/Library/RBT: red-black trees.
haftmann@26728
   163
wenzelm@26874
   164
* February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and
wenzelm@26874
   165
  Lukas Bulwahn, TUM and John Matthews, Galois:
wenzelm@26874
   166
  HOL/Library/Imperative_HOL: Haskell-style imperative data structures
wenzelm@26874
   167
  for HOL.
haftmann@26728
   168
wenzelm@27009
   169
* December 2007: Norbert Schirmer, Uni Saarbruecken
wenzelm@27009
   170
  Misc improvements of record package in HOL.
wenzelm@27009
   171
wenzelm@27009
   172
* December 2007: Florian Haftmann, TUM
wenzelm@27009
   173
  Overloading and class instantiation target.
wenzelm@27009
   174
wenzelm@27009
   175
* December 2007: Florian Haftmann, TUM
wenzelm@27009
   176
  New version of primrec package for local theories.
wenzelm@27009
   177
wenzelm@27009
   178
* December 2007: Alexander Krauss, TUM
wenzelm@27009
   179
  Method "induction_scheme" in HOL.
wenzelm@27009
   180
wenzelm@27009
   181
* November 2007: Peter Lammich, Uni Muenster
wenzelm@27009
   182
  HOL-Lattice: some more lemmas.
wenzelm@26198
   183
wenzelm@26874
   184
wenzelm@25454
   185
Contributions to Isabelle2007
wenzelm@25454
   186
-----------------------------
wenzelm@23252
   187
schirmer@25409
   188
* October 2007: Norbert Schirmer, TUM / Uni Saarbruecken
wenzelm@25398
   189
  State Spaces: The Locale Way (in HOL).
wenzelm@25398
   190
wenzelm@25057
   191
* October 2007: Mark A. Hillebrand, DFKI
wenzelm@25057
   192
  Robust sub/superscripts in LaTeX document output.
wenzelm@25057
   193
wenzelm@24799
   194
* August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian
wenzelm@24799
   195
    Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois
kleing@24333
   196
  HOL-Word: a library for fixed-size machine words in Isabelle.
kleing@24333
   197
kleing@24332
   198
* August 2007: Brian Huffman, PSU
wenzelm@24799
   199
  HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type.
kleing@24332
   200
wenzelm@23252
   201
* June 2007: Amine Chaieb, TUM
wenzelm@24799
   202
  Semiring normalization and Groebner Bases.
wenzelm@25449
   203
  Support for dense linear orders.
wenzelm@17866
   204
paulson@23449
   205
* June 2007: Joe Hurd, Oxford
wenzelm@24799
   206
  Metis theorem-prover.
wenzelm@24799
   207
wenzelm@24799
   208
* 2007: Kong W. Susanto, Cambridge
wenzelm@24799
   209
  HOL: Metis prover integration.
paulson@23449
   210
wenzelm@24799
   211
* 2007: Stefan Berghofer, TUM
wenzelm@25449
   212
  HOL: inductive predicates and sets.
wenzelm@24799
   213
wenzelm@24803
   214
* 2007: Norbert Schirmer, TUM
wenzelm@24803
   215
  HOL/record: misc improvements.
wenzelm@24803
   216
wenzelm@24799
   217
* 2006/2007: Alexander Krauss, TUM
wenzelm@24799
   218
  HOL: function package and related theories on termination.
paulson@23449
   219
haftmann@22449
   220
* 2006/2007: Florian Haftmann, TUM
haftmann@22449
   221
  Pure: generic code generator framework.
haftmann@22449
   222
  Pure: class package.
wenzelm@24799
   223
  HOL: theory reorganization, code generator setup.
wenzelm@24799
   224
wenzelm@25449
   225
* 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and
wenzelm@25449
   226
    Julien Narboux, TUM
wenzelm@24799
   227
  HOL/Nominal package and related tools.
haftmann@22449
   228
wenzelm@21242
   229
* November 2006: Lukas Bulwahn, TUM
wenzelm@24799
   230
  HOL: method "lexicographic_order" for function package.
wenzelm@21242
   231
wenzelm@21169
   232
* October 2006: Stefan Hohe, TUM
wenzelm@21169
   233
  HOL-Algebra: ideals and quotients over rings.
wenzelm@21169
   234
wenzelm@20340
   235
* August 2006: Amine Chaieb, TUM
wenzelm@20340
   236
  Experimental support for generic reflection and reification in HOL.
wenzelm@20340
   237
kleing@20067
   238
* July 2006: Rafal Kolanski, NICTA
kleing@20067
   239
  Hex (0xFF) and binary (0b1011) numerals.
kleing@20067
   240
nipkow@19896
   241
* May 2006: Klaus Aehlig, LMU
nipkow@19896
   242
  Command 'normal_form': normalization by evaluation.
nipkow@19896
   243
wenzelm@19650
   244
* May 2006: Amine Chaieb, TUM
wenzelm@19650
   245
  HOL-Complex: Ferrante and Rackoff Algorithm for linear real
wenzelm@19650
   246
  arithmetic.
kleing@19470
   247
kleing@19470
   248
* February 2006: Benjamin Porter, NICTA
kleing@23382
   249
  HOL and HOL-Complex: generalised mean value theorem, continuum is
kleing@19470
   250
  not denumerable, harmonic and arithmetic series, and denumerability
kleing@19470
   251
  of rationals.
wenzelm@17532
   252
wenzelm@19650
   253
* October 2005: Martin Wildmoser, TUM
wenzelm@19650
   254
  Sketch for Isar 'guess' element.
wenzelm@19650
   255
wenzelm@19650
   256
wenzelm@25454
   257
Contributions to Isabelle2005
wenzelm@25454
   258
-----------------------------
wenzelm@17382
   259
wenzelm@17640
   260
* September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
wenzelm@17640
   261
  HOL-Complex: Formalization of Taylor series.
wenzelm@17640
   262
wenzelm@17640
   263
* September 2005: Stephan Merz, Alwen Tiu, QSL Loria
wenzelm@17640
   264
  Components for SAT solver method using zChaff.
wenzelm@17640
   265
wenzelm@17534
   266
* September 2005: Ning Zhang and Christian Urban, LMU Munich
wenzelm@17534
   267
  A Chinese theory.
wenzelm@17534
   268
wenzelm@17562
   269
* September 2005: Bernhard Haeupler, TUM
wenzelm@17382
   270
  Method comm_ring for proving equalities in commutative rings.
wenzelm@16892
   271
wenzelm@17532
   272
* July/August 2005: Jeremy Avigad, Carnegie Mellon University
wenzelm@16892
   273
  Various improvements of the HOL and HOL-Complex library.
wenzelm@16868
   274
wenzelm@16892
   275
* July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
wenzelm@16892
   276
  Some structured proofs about completeness of real numbers.
wenzelm@16892
   277
wenzelm@17532
   278
* May 2005: Rafal Kolanski and Gerwin Klein, NICTA
wenzelm@17532
   279
  Improved retrieval of facts from theory/proof context.
wenzelm@15994
   280
wenzelm@16252
   281
* February 2005: Lucas Dixon, University of Edinburgh
wenzelm@17532
   282
  Improved subst method.
wenzelm@17532
   283
wenzelm@17532
   284
* 2005: Brian Huffman, OGI
wenzelm@17532
   285
  Various improvements of HOLCF.
wenzelm@17532
   286
  Some improvements of the HOL-Complex library.
wenzelm@17532
   287
wenzelm@17532
   288
* 2005: Claire Quigley and Jia Meng, University of Cambridge
wenzelm@17532
   289
  Some support for asynchronous communication with external provers
wenzelm@17532
   290
  (experimental).
wenzelm@17532
   291
wenzelm@17532
   292
* 2005: Florian Haftmann, TUM
wenzelm@17543
   293
  Contributions to document 'sugar'.
wenzelm@17532
   294
  Various ML combinators, notably linear functional transformations.
wenzelm@17532
   295
  Some cleanup of ML legacy.
wenzelm@17532
   296
  Additional antiquotations.
wenzelm@17532
   297
  Improved Isabelle web site.
wenzelm@17532
   298
wenzelm@17532
   299
* 2004/2005: David Aspinall, University of Edinburgh
wenzelm@17532
   300
  Various elements of XML and PGIP based communication with user
wenzelm@17532
   301
  interfaces (experimental).
wenzelm@17532
   302
wenzelm@17532
   303
* 2004/2005: Gerwin Klein, NICTA
wenzelm@17532
   304
  Contributions to document 'sugar'.
wenzelm@17532
   305
  Improved Isabelle web site.
wenzelm@17532
   306
  Improved HTML presentation of theories.
wenzelm@17532
   307
wenzelm@17532
   308
* 2004/2005: Clemens Ballarin, TUM
wenzelm@17532
   309
  Provers: tools for transitive relations and quasi orders.
wenzelm@17532
   310
  Improved version of locales, notably interpretation of locales.
wenzelm@17532
   311
  Improved version of HOL-Algebra.
wenzelm@17532
   312
wenzelm@17532
   313
* 2004/2005: Amine Chaieb, TUM
wenzelm@17532
   314
  Improved version of HOL presburger method.
wenzelm@17532
   315
wenzelm@17532
   316
* 2004/2005: Steven Obua, TUM
wenzelm@17532
   317
  Improved version of HOL/Import, support for HOL-Light.
wenzelm@17532
   318
  Improved version of HOL-Complex-Matrix.
wenzelm@17572
   319
  Pure/defs: more sophisticated checks on well-formedness of overloading.
wenzelm@17543
   320
  Pure/Tools: an experimental evaluator for lambda terms.
wenzelm@17532
   321
wenzelm@17532
   322
* 2004/2005: Norbert Schirmer, TUM
wenzelm@17532
   323
  Contributions to document 'sugar'.
wenzelm@17532
   324
  Improved version of HOL/record.
wenzelm@17532
   325
wenzelm@17532
   326
* 2004/2005: Sebastian Skalberg, TUM
wenzelm@17532
   327
  Improved version of HOL/Import.
wenzelm@17532
   328
  Some internal ML reorganizations.
wenzelm@17532
   329
wenzelm@17532
   330
* 2004/2005: Tjark Weber, TUM
wenzelm@17640
   331
  SAT solver method using zChaff.
wenzelm@17532
   332
  Improved version of HOL/refute.