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