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