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