Skip to content

Changes

#96 (Mar 20, 2022, 12:14:00 AM)

  1. Tidied several ugly proofs in some elderly examples — paulson <lp15@cam.ac.uk> / hgweb
  2. tuned message; — wenzelm / hgweb
  3. clarified errors; — wenzelm / hgweb
  4. tuned messages; — wenzelm / hgweb
  5. support Node.js as well, reusing the engine from Electron/VSCodium; — wenzelm / hgweb
  6. updated to vscode 1.65.2; — wenzelm / hgweb
  7. proper result check; — wenzelm / hgweb
  8. merged — wenzelm / hgweb
  9. clarified directory layout and settings: more robust on all platforms; — wenzelm / hgweb
  10. tuned; — wenzelm / hgweb
  11. support Electron application framework;
    clarified vscodium startup; — wenzelm / hgweb
  12. generated lemma map_ident_strong for BNFs — desharna / hgweb
  13. updated SMT certificates — desharna / hgweb
  14. used more descriptive assert names in SMT-Lib output — desharna / hgweb

#95 (Mar 13, 2022, 12:14:00 AM)

  1. clarified and unified executable names; — wenzelm / hgweb
  2. tuned; — wenzelm / hgweb
  3. tuned; — wenzelm / hgweb
  4. merged — wenzelm / hgweb
  5. suppress OCaml icons: avoid conflict of .ml and .ML, due to case-insensitive file-names in VSCode; — wenzelm / hgweb
  6. fix handling of lambdas in reconstruction of eq_congruent — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
  7. more robust: avoid breakdown of Search dialog; — wenzelm / hgweb
  8. tuned; — wenzelm / hgweb
  9. always use Isabelle encoding, as in Isabelle/jEdit; — wenzelm / hgweb
  10. tuned signature; — wenzelm / hgweb
  11. clarified signature: more uniform ts vs. Scala; — wenzelm / hgweb
  12. discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249;
    discontinued special treatment of workspace_dir as session directory; — wenzelm / hgweb
  13. actually decode/encode symbols; — wenzelm / hgweb
  14. merged — wenzelm / hgweb
  15. prefer yarn over npm; — wenzelm / hgweb
  16. more accurate .hgignore; — wenzelm / hgweb
  17. clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode; — wenzelm / hgweb
  18. tuned messages; — wenzelm / hgweb
  19. proper init_resources for macos; — wenzelm / hgweb
  20. clarified names; — wenzelm / hgweb
  21. clarified modules: vscode vs. extension;
    clarified signature; — wenzelm / hgweb
  22. inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs; — wenzelm / hgweb
  23. more operations; — wenzelm / hgweb
  24. tuned comments;
    tuned messages; — wenzelm / hgweb
  25. patch VSCode source tree to support isabelle_encoding.ts; — wenzelm / hgweb
  26. more robust, pass "yarn valid-layers-check"; — wenzelm / hgweb
  27. clarified directories; — wenzelm / hgweb
  28. patch for vscode encoding "UTF-8-Isabelle": clone of "utf8", no symbols yet; — wenzelm / hgweb
  29. fit into vscode source conventions; — wenzelm / hgweb
  30. A tiny further cleanup — paulson <lp15@cam.ac.uk> / hgweb
  31. Tidied some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
  32. merged — nipkow / hgweb
  33. more count_list lemmas — nipkow / hgweb
  34. towards UTF-8-Isabelle symbol encoding; — wenzelm / hgweb
  35. updated to VSCode 1.65.0; — wenzelm / hgweb
  36. clarified char symbols: cover most European languages; — wenzelm / hgweb
  37. more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML); — wenzelm / hgweb
  38. tuned comments;
    tuned imports; — wenzelm / hgweb
  39. more robust dependencies: avoid implicit update, escpecially of underlying vscode engine; — wenzelm / hgweb
  40. proper file headers; — wenzelm / hgweb
  41. added count_list lemmas — nipkow / hgweb
  42. tuned message; — wenzelm / hgweb
  43. more compact result; — wenzelm / hgweb
  44. prepare patched version more thoroughly, with explicit patches; — wenzelm / hgweb
  45. tuned signature; — wenzelm / hgweb

#95 (Mar 13, 2022, 12:14:00 AM)

  1. more count_list lemmas — nipkow / hgweb
  2. more count_list — nipkow / hgweb
  3. merged — nipkow / hgweb
  4. moved some count_list lemmas — nipkow / hgweb
  5. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
  6. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
  7. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
  8. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
  9. continue 98838b260ed4 — Frédéric Tuong / hgweb
  10. continue ee01bce2ecca — Frédéric Tuong / hgweb
  11. cancel some part of 11d4567f1b99 — Frédéric Tuong / hgweb
  12. cancel some part of 98838b260ed4 — Frédéric Tuong / hgweb
  13. cancel some part of ada85c62541d — Frédéric Tuong / hgweb
  14. synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb

#94 (Mar 6, 2022, 12:14:00 AM)

  1. recover platform-specific node binaries from original download, notably for node-pty for Terminal; — wenzelm / hgweb
  2. tuned message; — wenzelm / hgweb
  3. tuned; — wenzelm / hgweb
  4. tuned imports; — wenzelm / hgweb
  5. misc tuning and clarification; — wenzelm / hgweb
  6. more executable files;
    clarified modules; — wenzelm / hgweb
  7. tuned; — wenzelm / hgweb
  8. tuned output; — wenzelm / hgweb
  9. clarified signature; — wenzelm / hgweb
  10. tuned, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
  11. tuned; — wenzelm / hgweb
  12. clarified command-line options; — wenzelm / hgweb
  13. update official Isabelle release, notably for "Admin/init -R"; — wenzelm / hgweb
  14. more robust; — wenzelm / hgweb
  15. build component for VSCodium (cross-compiled from sources for all platforms); — wenzelm / hgweb
  16. tuned signature: more robust operation; — wenzelm / hgweb
  17. clarified order; — wenzelm / hgweb
  18. proper antiquotations (amending ff784d5a5bfb); — wenzelm / hgweb
  19. clarified signature: file operations take standard_path as in Isabelle/ML/Scala; — wenzelm / hgweb
  20. provide symbols statically via ISABELLE_VSCODE_WORKSPACE, instead of LSP/PIDE protocol; — wenzelm / hgweb
  21. proper init of non-existing file; — wenzelm / hgweb
  22. proper function call; — wenzelm / hgweb
  23. clarified signature; — wenzelm / hgweb
  24. tuned; — wenzelm / hgweb
  25. tuned, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
  26. tuned; — wenzelm / hgweb
  27. clarified signature; — wenzelm / hgweb
  28. clarified modules: more uniform .scala vs. ts (amending 4519eeefe3b5); — wenzelm / hgweb
  29. misc tuning, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
  30. clarified signature; — wenzelm / hgweb
  31. tuned signature; — wenzelm / hgweb
  32. clarified signature;
    clarified data structures; — wenzelm / hgweb
  33. tuned imports; — wenzelm / hgweb
  34. clarified signature; — wenzelm / hgweb
  35. clarified signature; — wenzelm / hgweb
  36. tuned signature; — wenzelm / hgweb
  37. misc tuning, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
  38. clarified modules; — wenzelm / hgweb
  39. support for file-system operations; — wenzelm / hgweb
  40. tuned signature; — wenzelm / hgweb
  41. follow standard Isabelle license --- no longer published on market place; — wenzelm / hgweb
  42. tuned README; — wenzelm / hgweb
  43. disregard public marketplace; — wenzelm / hgweb
  44. tuned imports; — wenzelm / hgweb
  45. more robust; — wenzelm / hgweb
  46. merged — wenzelm / hgweb
  47. tuned message; — wenzelm / hgweb
  48. clarified module; — wenzelm / hgweb
  49. tuned comments; — wenzelm / hgweb
  50. added documentation for new VSCode modules; — Fabian Huch <huch@in.tum.de> / hgweb
  51. proper monospace font for terminal; — wenzelm / hgweb
  52. merged — wenzelm / hgweb
  53. tuned; — wenzelm / hgweb
  54. support system path representations (as in Isabelle/Java/Scala); — wenzelm / hgweb
  55. auto-update; — wenzelm / hgweb
  56. more robust; — wenzelm / hgweb
  57. clarified modules; — wenzelm / hgweb
  58. clarified rendering; — wenzelm / hgweb
  59. prefer hardwired locale; — wenzelm / hgweb
  60. more aggressive activation; — wenzelm / hgweb
  61. Added some theorems (from Wetzel) — paulson <lp15@cam.ac.uk> / hgweb
  62. tuned; — wenzelm / hgweb
  63. tuned; — wenzelm / hgweb
  64. tuned message; — wenzelm / hgweb
  65. disable extension updates; — wenzelm / hgweb
  66. tuned message; — wenzelm / hgweb
  67. disable check for updates: support just one static version; — wenzelm / hgweb
  68. misc tuning based on comments by Heiko Eißfeldt; — wenzelm / hgweb
  69. misc tuning based on comments by Heiko Eißfeldt; — wenzelm / hgweb

#94 (Mar 6, 2022, 12:14:00 AM)

  1. split locale in two — desharna / hgweb
  2. Stronger strong completeness result and variant that uses variables as Henkin witnesses. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  3. Stronger strong completeness result and variant that uses variables as Henkin witnesses. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  4. added some alternative proofs in Smith_Normal_Form entry — jodivaso / hgweb
  5. The last tranche of material to be moved to the complex analysis libraries — paulson <lp15@cam.ac.uk> / hgweb
  6. Removal of material that has since been added to ZFC_in_HOL.General_Cardinals — paulson <lp15@cam.ac.uk> / hgweb

#93 (Feb 27, 2022, 12:14:00 AM)

  1. removed junk; — wenzelm / hgweb
  2. some updates to README.md; — wenzelm / hgweb
  3. clarified default settings; — wenzelm / hgweb
  4. tuned whitespace; — wenzelm / hgweb
  5. support Isabelle fonts via patch of vscode resources; — wenzelm / hgweb
  6. proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249); — wenzelm / hgweb
  7. clarified symbolic path; — wenzelm / hgweb
  8. clarified extension name (again); — wenzelm / hgweb
  9. removed obsolete material; — wenzelm / hgweb
  10. update scripts, based on recent "yo code" template; — wenzelm / hgweb
  11. clarified extension name (again), corresponding to qualified resources within VSCode (settings, commands, etc.); — wenzelm / hgweb
  12. clarified signature; — wenzelm / hgweb
  13. clarified extension name; — wenzelm / hgweb
  14. clarified signature; — wenzelm / hgweb
  15. clarified signature; — wenzelm / hgweb
  16. clarified options; — wenzelm / hgweb
  17. support local .vsix installation;
    discontinued publishing to VSCode Marketplace, which will become obsolete eventually; — wenzelm / hgweb
  18. formal record of generated package-lock.json; — wenzelm / hgweb
  19. pro-forma update of version, for ongoing development; — wenzelm / hgweb
  20. updated notes on Isabelle/VSCode development; — wenzelm / hgweb
  21. proper engines.vscode (amending c04ccea8bdd2): required for "vsce package", e.g. via "isabelle build_vscode; — wenzelm / hgweb
  22. simp rules for negative numerals — haftmann / hgweb
  23. updated vscode extension: proper recoding; — Fabian Huch <huch@in.tum.de> / hgweb
  24. tuned vscode extension; — Fabian Huch <huch@in.tum.de> / hgweb
  25. tuned vscode extension: split isabelle fsp into workspace and mapping; — Fabian Huch <huch@in.tum.de> / hgweb
  26. update VSCode plugin dependencies; — Fabian Huch <huch@in.tum.de> / hgweb
  27. added Isabelle output panel to VSCode extension; — Fabian Huch <huch@in.tum.de> / hgweb
  28. Simplified a couple of extremely long and ugly apply-proofs — paulson <lp15@cam.ac.uk> / hgweb
  29. merged — wenzelm / hgweb
  30. some updates to README.md; — wenzelm / hgweb
  31. refer to Isabelle settings via environment, which is provided via "isabelle vscode";
    clarified error handling; — wenzelm / hgweb
  32. more operations; — wenzelm / hgweb
  33. more robust startup wrt. VSCode workspace (by Fabian Huch); — wenzelm / hgweb
  34. various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch); — wenzelm / hgweb
  35. have Sledgehammer honor 'smt_nat_as_int' option — blanchet / hgweb
  36. more handling of Zipperposition definitions in Isar proof construction — blanchet / hgweb
  37. handle Zipperposition definitions in Isar proof construction — blanchet / hgweb
  38. parse Zipperposition definitions — blanchet / hgweb
  39. clarified URL; — wenzelm / hgweb
  40. clarified pdf path; — wenzelm / hgweb
  41. HTTP view of Isabelle PDF documentation; — wenzelm / hgweb
  42. clarified signature; — wenzelm / hgweb
  43. more robust; — wenzelm / hgweb
  44. tuned message; — wenzelm / hgweb
  45. clarified signature: more explicit section structure; — wenzelm / hgweb
  46. clarified signature; — wenzelm / hgweb
  47. clarified signature; — wenzelm / hgweb
  48. tuned signature; — wenzelm / hgweb
  49. tuned; — wenzelm / hgweb
  50. clarified URL (again); — wenzelm / hgweb
  51. more robust toplevel url: allow extra "/"; — wenzelm / hgweb
  52. clarified signature; — wenzelm / hgweb
  53. clarified signature;
    clarified URLs; — wenzelm / hgweb
  54. clarified signature; — wenzelm / hgweb
  55. support for PDF.js: platform-independent PDF viewer; — wenzelm / hgweb
  56. more robust mime_type; — wenzelm / hgweb
  57. merged — wenzelm / hgweb
  58. improved support for Java Chromium Embedded Framework (JCEF): works on x86_64-linux and x86_64-windows with jdk-15 (not jdk-17), does not work on arm64 and darwin; — wenzelm / hgweb
  59. one new lemma — paulson <lp15@cam.ac.uk> / hgweb
  60. clarified options; — wenzelm / hgweb
  61. clarified options; — wenzelm / hgweb
  62. clarified directory; — wenzelm / hgweb
  63. tuned whitespace; — wenzelm / hgweb
  64. prefer strict equality, without implicit type conversion; — wenzelm / hgweb
  65. tuned; — wenzelm / hgweb
  66. auto-update by VSCode; — wenzelm / hgweb
  67. more activationEvents, as proposed by Denis Paluca; — wenzelm / hgweb
  68. tuned message; — wenzelm / hgweb
  69. NEWS; — wenzelm / hgweb
  70. run Isabelle/VSCode using local VSCodium installation; — wenzelm / hgweb
  71. provide macos_exe, based on bin/codium from linux; — wenzelm / hgweb
  72. clarified options; — wenzelm / hgweb
  73. Avoid overaggresive splitting. — haftmann / hgweb
  74. more lemmas for distribution — haftmann / hgweb
  75. Avoid overaggresive simplification. — haftmann / hgweb
  76. merged — wenzelm / hgweb
  77. setup VSCode from VSCodium distribution; — wenzelm / hgweb
  78. more robust package_dir, to increase chances that it works with IntelliJ IDEA; — wenzelm / hgweb
  79. NEWS — desharna / hgweb
  80. Mirabelle now considers goals preceding "unfolding" and "using" commands — desharna / hgweb

#93 (Feb 27, 2022, 12:14:00 AM)

  1. Deleted nearly 200 lines of unused material — paulson <lp15@cam.ac.uk> / hgweb
  2. A new theorem — paulson <lp15@cam.ac.uk> / hgweb
  3. Clarified code module names. — haftmann / hgweb
  4. removed ancient numeral representation — haftmann / hgweb
  5. restore state of VYDRA_MDL to b8c3f69745a4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  6. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  7. metadata for Universal_Hash_Families — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  8. new entry Universal_Hash_Families — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  9. New entry Wetzel's Problem — nipkow / hgweb
  10. metadata for Eval_FO — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  11. new entry Eval_FO — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  12. metadata for VYDRA_MDL — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  13. new entry VYDRA_MDL — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  14. Backed out changeset c9f94b0ae10e — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  15. Backed out changeset b8c3f69745a4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  16. metadata update for VYDRA_MDL — mraszyk / hgweb
  17. New entry: VYDRA_MDL — mraszyk / hgweb
  18. fixed failing proofs — desharna / hgweb
  19. New definition of the Aleph operator so that it's defined for all arguments,  not just ordinals — paulson <lp15@cam.ac.uk> / hgweb
  20. ALEXANDRIA acknowledgements — paulson <lp15@cam.ac.uk> / hgweb
  21. merged — paulson / hgweb
  22. New set theory lemmas about cardinality (mainly) — paulson <lp15@cam.ac.uk> / hgweb
  23. Another attempt for a consolidated terminology. — haftmann / hgweb
  24. Avoid overaggresive splitting. — haftmann / hgweb
  25. more lemmas for distribution — haftmann / hgweb
  26. Avoid overaggresive simplification. — haftmann / hgweb
  27. some new lemmas — paulson <lp15@cam.ac.uk> / hgweb

#92 (Feb 20, 2022, 12:14:00 AM)

  1. merged — paulson / hgweb
  2. an assortment of new or stronger lemmas — paulson <lp15@cam.ac.uk> / hgweb
  3. obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented; — wenzelm / hgweb
  4. print outcome of Sledgehammer search in panel — blanchet / hgweb
  5. print Sledgehammer error message — blanchet / hgweb

#92 (Feb 20, 2022, 12:14:00 AM)

  1. merged — nipkow / hgweb
  2. More material — nipkow / hgweb
  3. added idempotent most general unifier — desharna / hgweb
  4. used same parameter order for locales substitution and substitution — desharna / hgweb
  5. patched for new/simplified lemmas — paulson <lp15@cam.ac.uk> / hgweb
  6. Better notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb

#91 (Feb 13, 2022, 12:14:00 AM)

  1. updated documentation to current matter of affairs — haftmann / hgweb
  2. unused; — wenzelm / hgweb
  3. clarified signature; — wenzelm / hgweb
  4. merged — desharna / hgweb
  5. added Isabelle identification to Mirabelle output — desharna / hgweb
  6. uniformized fact selection for ATP and SMT in Sledgehammer — desharna / hgweb
  7. provide cache for slow computations; — wenzelm / hgweb
  8. used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer — desharna / hgweb
  9. more operations; — wenzelm / hgweb
  10. more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson) — blanchet / hgweb
  11. more robust TSTP proof parsing — blanchet / hgweb
  12. added possibility of extra options to SMT slices — blanchet / hgweb

#91 (Feb 13, 2022, 12:14:00 AM)

  1. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  2. avoid conflict with index.html in generated html — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  3. New entry: FO_Theory_Rewriting — nipkow / hgweb
  4. Improve consistency of type-variables in WOOT_Strong_Eventual_Consistency.

    + Remove obsolete e-mail from notification mailing list. — Emin Karayel <me@eminkarayel.de> / hgweb
  5. Improve proofs for Interpolation_Polynomials_HOL_Algebra.

    Reduced the number of apply scripts used. — Emin Karayel <me@eminkarayel.de> / hgweb
  6. Correct date. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  7. deleted a lemma that's in the devel library — paulson <lp15@cam.ac.uk> / hgweb
  8. Cleanup and new results. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  9. moved theorems into Matrix.thy — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  10. merge of AFP 2021-1 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  11. New AFP entry: Equivalence_Relation_Enumeration — nipkow / hgweb
  12. new entry: LP_Duality — nipkow / hgweb
  13. cosmetic tweaks — paulson <lp15@cam.ac.uk> / hgweb
  14. sitegen and metadata for Young's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  15. new entry: Young's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  16. metadata for Quasi_Borel_Spaces, sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  17. new entry: Quasi_Borel_Spaces — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  18. sitegen for FOL_Seq_Calc2 — paulson <lp15@cam.ac.uk> / hgweb
  19. new entry FOL_Seq_Calc2 — paulson <lp15@cam.ac.uk> / hgweb
  20. tweak: corollary that the ln also yields irrational numbers — paulson <lp15@cam.ac.uk> / hgweb
  21. New entry: Interpolation_Polynomials_HOL_Algebra — nipkow / hgweb
  22. Finally remembered to run sitegen — paulson <lp15@cam.ac.uk> / hgweb
  23. Fixed the meta data in the abstract as well — paulson <lp15@cam.ac.uk> / hgweb
  24. Eliminated the references to SOS (which is no longer used) and changed to the document style to "article". — paulson <lp15@cam.ac.uk> / hgweb
  25. typo — nipkow / hgweb
  26. typo — nipkow / hgweb
  27. New entry Irrationals_From_THEBOOK — nipkow / hgweb
  28. new entry Median_Method — nipkow / hgweb
  29. Actuarial Mathematics website — paulson <lp15@cam.ac.uk> / hgweb
  30. New entry Actuarial_Mathematics — paulson <lp15@cam.ac.uk> / hgweb

#90 (Feb 6, 2022, 12:14:00 AM)

  1. tuned output syntax: Hoare triples are now blocks — nipkow / hgweb
  2. tuned output syntax: INV and VAR are now blocks — nipkow / hgweb
  3. more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)') — blanchet / hgweb
  4. enable induction in one of Zipperposition's slices — blanchet / hgweb
  5. made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme — blanchet / hgweb
  6. robustly handle empty proof blocks in Isar proof output — blanchet / hgweb
  7. propagate right result when enough proofs have been found — blanchet / hgweb
  8. correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives — blanchet / hgweb
  9. don't lose error messages — blanchet / hgweb
  10. don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice — blanchet / hgweb
  11. careful with partial applications — blanchet / hgweb
  12. don't perform preplaying steps if preplaying is disabled — blanchet / hgweb
  13. adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs — blanchet / hgweb
  14. tuned punctuation — blanchet / hgweb
  15. handle TPTP '!=' more gracefully in Isar proof reconstruction — blanchet / hgweb
  16. guard against duplicate lines in Zipperposition proofs — blanchet / hgweb
  17. tuning — blanchet / hgweb
  18. tuned NEWS — blanchet / hgweb
  19. compile HOL-TPTP — blanchet / hgweb
  20. compile Metis_Examples — blanchet / hgweb
  21. more NEWS — blanchet / hgweb
  22. compile mirabelle — blanchet / hgweb
  23. tweaked Auto Sledgehammer's behavior and output — blanchet / hgweb
  24. updated NEWS — blanchet / hgweb
  25. removed experimental prover z3_tptp — blanchet / hgweb
  26. print more verbose information — blanchet / hgweb
  27. run all installed provers by default — blanchet / hgweb
  28. update slice options centrally — blanchet / hgweb
  29. further work on new Sledgehammer slicing — blanchet / hgweb
  30. tweaked verbose output — blanchet / hgweb
  31. tweak padding of prover slice schedule to include all provers — blanchet / hgweb
  32. implemented 'max_proofs' mechanism — blanchet / hgweb
  33. document new option 'max_proofs' — blanchet / hgweb
  34. crude implementation of centralized slicing — blanchet / hgweb
  35. removed obscure E option — blanchet / hgweb
  36. take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set — blanchet / hgweb
  37. rationalize slicing format — blanchet / hgweb
  38. thread slices through — blanchet / hgweb
  39. simplified 'best_slice' data structure and made minor changes to slices — blanchet / hgweb
  40. changed logic of 'slice' option to 'slices' — blanchet / hgweb
  41. updated documentation of 'slice' (now 'slices') option — blanchet / hgweb
  42. revised Sledgehammer documentation — blanchet / hgweb
  43. rationalized output for forthcoming slicing model — blanchet / hgweb
  44. use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code — blanchet / hgweb
  45. disable slicing within ATP module (in preparation for refactoring) — blanchet / hgweb
  46. disable slicing within SMT (in preparation for factoring it out) — blanchet / hgweb
  47. generalized the 'slice' option towards more flexible slicing — blanchet / hgweb
  48. tuned -- fewer warnings; — wenzelm / hgweb

#90 (Feb 6, 2022, 12:14:00 AM)

  1. Strong soundness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  2. Strong soundness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  3. Fix LaTeX issue. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  4. Qualification required(?) — nipkow / hgweb
  5. merged — nipkow / hgweb
  6. more variants of the algorithm — nipkow / hgweb
  7. Added funding acknowledgments.
    Fixed broken BibTeX citation. — Dominique Unruh <unruh@ut.ee> / hgweb
  8. Strong completeness for PAL systems. — Asta Halkjær From <andro.from@gmail.com> / hgweb

#89 (Jan 30, 2022, 12:14:00 AM)

  1. Added a tiny proof — paulson <lp15@cam.ac.uk> / hgweb
  2. Deletion of a duplicate proof — paulson <lp15@cam.ac.uk> / hgweb
  3. useful lemma integral_less — paulson <lp15@cam.ac.uk> / hgweb
  4. merged — desharna / hgweb
  5. removed unused parameter following f9908452b282 — desharna / hgweb
  6. treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis) — blanchet / hgweb
  7. fixed dodgy intro! attributes — paulson <lp15@cam.ac.uk> / hgweb
  8. merged — desharna / hgweb
  9. optimized facts traversal in TPTP translation — desharna / hgweb
  10. optimized app_op_level selection in TPTP generation — desharna / hgweb
  11. tuned trivial check in mirabelle_sledgehammer — desharna / hgweb
  12. renamed run_action to run in Mirabelle.action record — desharna / hgweb
  13. added spying of fact filtering timing — desharna / hgweb
  14. tuned mirabelle_sledgehammer output — desharna / hgweb
  15. added spying to Sledgehammer — desharna / hgweb
  16. proper fact filter for dummy ATPs — desharna / hgweb
  17. added syping of fact filtering time to sledgehammer — desharna / hgweb
  18. removed unsynchronized references in mirabelle_sledgehammer — desharna / hgweb
  19. tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run — desharna / hgweb
  20. updated to polyml-test-15c840d48c9a; — wenzelm / hgweb

#89 (Jan 30, 2022, 12:14:00 AM)

  1. Cleanup. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  2. Fewer parentheses around turnstile + remove unused lemmas. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  3. Simplify proof of truth lemma. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  4. Notation for `imply` and fewer parenthesis around turnstiles. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  5. Abstract results to shorten proofs. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  6. Better notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  7. merged — wenzelm / hgweb
  8. tuned whitespace; — wenzelm / hgweb
  9. more symbols; — wenzelm / hgweb
  10. profer bundle lattice_syntax; — wenzelm / hgweb
  11. prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation' as intended; — wenzelm / hgweb
  12. Add soundness and completeness for the PAL versions of systems K, T, KB, K4, S4 and S5. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  13. avoid hardwired document output; — wenzelm / hgweb
  14. merged — paulson / hgweb
  15. deleting the overloading of div and mod, with its attendant ambiguities — paulson <lp15@cam.ac.uk> / hgweb
  16. replaced Erdős by Erd\H{o}s (fixed problem in LaTeX document generation) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb

#88 (Jan 23, 2022, 12:14:00 AM)

  1. some updates and clarification on Assumption.export_term; — wenzelm / hgweb
  2. new theorem has_integral_UN — paulson <lp15@cam.ac.uk> / hgweb
  3. updated to jdk-17.0.2+8; — wenzelm / hgweb
  4. used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads — desharna / hgweb
  5. NEWS — desharna / hgweb
  6. added Mirabelle option "-y" for dry run — desharna / hgweb
  7. tuned garbage optimization — desharna / hgweb
  8. added cpu time (in ms) to Mirabelle run_action output — desharna / hgweb
  9. added Mirabelle option -r to randomize the goals before selection — desharna / hgweb
  10. A new lemma about inverse image — paulson <lp15@cam.ac.uk> / hgweb
  11. proper treatment of $let variables in symbol table in Sledgehammer — desharna / hgweb
  12. removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer — desharna / hgweb

#88 (Jan 23, 2022, 12:14:00 AM)

  1. Removal of a lemma (now in the libraries) and a few tweaks — paulson <lp15@cam.ac.uk> / hgweb

#87 (Jan 16, 2022, 12:14:00 AM)

  1. merged — desharna / hgweb
  2. split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir" — desharna / hgweb
  3. proper name mangling of "undefined" constants in Sledgehammer — desharna / hgweb
  4. earlier availability of lifting — haftmann / hgweb
  5. more correct transfer — haftmann / hgweb
  6. merged — desharna / hgweb
  7. proper abstraction of function variables when instantiating induction rules in Sledgehammer — desharna / hgweb
  8. added lemma asympD — desharna / hgweb
  9. added lemma — nipkow / hgweb
  10. Some lemmas about continuous functions with integral zero — paulson <lp15@cam.ac.uk> / hgweb

#87 (Jan 16, 2022, 12:14:00 AM)

  1. Tuning. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  2. merged — paulson / hgweb
  3. tweaks — paulson <lp15@cam.ac.uk> / hgweb
  4. merged — paulson / hgweb
  5. Fixed an inadequate description — paulson <lp15@cam.ac.uk> / hgweb
  6. tuned — haftmann / hgweb
  7. mv to distribution — nipkow / hgweb
  8. by now in distribution — nipkow / hgweb
  9. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  10. fixed abstract — nipkow / hgweb
  11. tuned — nipkow / hgweb
  12. website and metadata for Hyperdual — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  13. new entry: Hyperdual — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  14. sorted ROOTS — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  15. tuned — nipkow / hgweb
  16. New entry Knights_Tour — nipkow / hgweb
  17. more thoroughly replace Michael Foster's e-mail address — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  18. metadata and sitegen for Gale_Shapley — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  19. new entry Gale_Shapley — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  20. update Michael Forster's email address — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  21. metadata and sitegen for Roth_Arithmetic_Progressions — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  22. new entry Roth_Arithmetic_Progressions — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  23. typo — nipkow / hgweb
  24. merged — nipkow / hgweb
  25. New entry Regular_Tree_Relations — nipkow / hgweb
  26. We DON'T want an output directory — paulson <lp15@cam.ac.uk> / hgweb
  27. MDP-Algorithms website — paulson <lp15@cam.ac.uk> / hgweb
  28. new entry MDP-Algorithms — paulson <lp15@cam.ac.uk> / hgweb
  29. typo — paulson <lp15@cam.ac.uk> / hgweb
  30. new entry MDP-Rewards — paulson <lp15@cam.ac.uk> / hgweb
  31. fixed typo — paulson <lp15@cam.ac.uk> / hgweb

#86 (Jan 9, 2022, 12:14:00 AM)

  1. merged — desharna / hgweb
  2. added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp — desharna / hgweb
  3. removed $ite from E 2.6 in THF format — desharna / hgweb
  4. New and simplified theorems — paulson <lp15@cam.ac.uk> / hgweb
  5. merged — desharna / hgweb
  6. prefixed all mirabelle_sledgehammer output lines with sledgehammer output — desharna / hgweb

#86 (Jan 9, 2022, 12:14:00 AM)

  1. CS: possibility to disable backtracking; CZH: auxiliary results; ETTS: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
  2. used wfP_imp_asymp from HOL — desharna / hgweb
  3. simplified proof some more — desharna / hgweb
  4. simplified proof — desharna / hgweb
  5. Extended protocol model to support composition of more than two protocols without
    the need of re-labeling them, additional automated checks, tighter integration
    of the stateful protocol model and the automated verification (PSPSP) tool. — Achim D. Brucker <adbrucker@0x5f.org> / hgweb

#85 (Jan 2, 2022, 12:14:00 AM)

  1. added lemma — nipkow / hgweb
  2. Tiny additions inspired by Roth development — paulson <lp15@cam.ac.uk> / hgweb

#85 (Jan 2, 2022, 12:14:00 AM)

  1. Tweaked some failing proofs — paulson <lp15@cam.ac.uk> / hgweb

#84 (Dec 26, 2021, 12:14:00 AM)

  1. allow general command transactions with presentation; — wenzelm / hgweb
  2. more operations; — wenzelm / hgweb
  3. clarified signature; — wenzelm / hgweb
  4. tuned signature; — wenzelm / hgweb
  5. support Gradle as alternative to Maven (again); — wenzelm / hgweb
  6. tuned mirabelle command-line help message — desharna / hgweb
  7. updated Mirabelle documentation — desharna / hgweb
  8. proper documentation for induction_rules Sledgehammer option — desharna / hgweb
  9. NEWS — desharna / hgweb
  10. merged — desharna / hgweb
  11. used TH1 for Leo-III in sledgehammer — desharna / hgweb
  12. tuned run_sledgehammer and called it directly from Mirabelle — desharna / hgweb
  13. exported Sledgehammer.launch_prover and use it in Mirabelle — desharna / hgweb
  14. proper filtering inf induction rules in Mirabelle — desharna / hgweb
  15. added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle — desharna / hgweb
  16. tuned ATP to use is_widely_irrelevant_const — desharna / hgweb
  17. added support for initialization messages to Mirabelle — desharna / hgweb

#84 (Dec 26, 2021, 12:14:00 AM)

  1. adapted to new Sledgehammer.run_sledgehammer return type — desharna / hgweb

#83 (Dec 19, 2021, 12:14:00 AM)

  1. tuned comment — blanchet / hgweb
  2. support for JSON:API; — wenzelm / hgweb
  3. support for Flarum server; — wenzelm / hgweb
  4. tuned whitespace; — wenzelm / hgweb
  5. tuned imports; — wenzelm / hgweb
  6. tuned comments; — wenzelm / hgweb
  7. clarified author names; — wenzelm / hgweb
  8. clarified author names; — wenzelm / hgweb
  9. merged — wenzelm / hgweb
  10. more accurate names;
    complete coverage of mail addresses; — wenzelm / hgweb
  11. more standard author_info; — wenzelm / hgweb
  12. clarified author info and cluster nodes; — wenzelm / hgweb
  13. more data integrity: name vs. address; — wenzelm / hgweb
  14. clarified signature: more operations; — wenzelm / hgweb
  15. clarified signature; — wenzelm / hgweb
  16. tuned; — wenzelm / hgweb
  17. more data integrity: name vs. address; — wenzelm / hgweb
  18. tuned comments; — wenzelm / hgweb
  19. merged — desharna / hgweb
  20. tuned ATP to use fold_index — desharna / hgweb
  21. tuned sledgehammer to use map_index — desharna / hgweb
  22. merged — wenzelm / hgweb
  23. more data integrity: name vs. address; — wenzelm / hgweb
  24. misc tuning and clarification; — wenzelm / hgweb
  25. clarified name; — wenzelm / hgweb
  26. more mailing list content; — wenzelm / hgweb
  27. more mailing list content; — wenzelm / hgweb
  28. updated links; — wenzelm / hgweb
  29. added Apache Commons Lang + Text: not particularly exciting, but provides useful things like org.apache.commons.text.StringEscapeUtils or org.apache.commons.text.diff; — wenzelm / hgweb
  30. tuned ATP to use map_index — desharna / hgweb
  31. removed obsolete RC tags; — wenzelm / hgweb
  32. proper path; — wenzelm / hgweb
  33. merged, resolving conflict in src/Doc/Implementation/Logic.thy; — wenzelm / hgweb
  34. Added tag Isabelle2021-1 for changeset c2a2be496f35 — wenzelm / hgweb
  35. tuned; — wenzelm / hgweb
  36. proper ML types (amending 1aa92bc4d356); — wenzelm / hgweb
  37. proper types for Scala.Fun instances (amending 1aa92bc4d356); — wenzelm / hgweb
  38. proper syntax category; — wenzelm / hgweb

#83 (Dec 19, 2021, 12:14:00 AM)

  1. Strengthened a lemma — paulson <lp15@cam.ac.uk> / hgweb
  2. updated the definition of scheme — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
  3. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  4. add change history — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  5. updated 2021-1 release dates -> web — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  6. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  7. ignore generated files — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  8. add 2021-1 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  9. set devel version again — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  10. Added tag Isabelle2021-1 for changeset 11f8b03a88ad — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  11. adjust usage version — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  12. set release version — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  13. update release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  14. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  15. The version without integer indexes — paulson <lp15@cam.ac.uk> / hgweb
  16. The version without integer indexes — paulson <lp15@cam.ac.uk> / hgweb
  17. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  18. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  19. new entry Foundation_of_geometry — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  20. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  21. Modified all design locale parameters to be nats instead of ints. Fixed proofs as required. — cledmonds / hgweb
  22. adjust for Isabelle2021-1-RC5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  23. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  24. new entry Simplicial_complexes_and_boolean_functions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  25. Modified all design locale parameters to be nats instead of ints. Fixed proofs as required. — cledmonds / hgweb
  26. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  27. adjust to Isabelle2021-1-RC5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  28. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  29. metadata and sitegen for Hahn_Jordan_Decomposition — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  30. added Mathematics/Measure theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  31. new entry: Hahn_Jordan_Decomposition — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  32. New entry: Van_Emde_Boas_Trees — nipkow / hgweb
  33. New entry: Van_Emde_Boas_Trees — nipkow / hgweb
  34. metadata and sitegen for SimplifiedOntologicalArgument — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  35. new entry: SimplifiedOntologicalArgument — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  36. Tuned: use a star in witness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  37. Rename H to S in maximal_exactly_one. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  38. Get rid of the sat abbreviation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  39. Add missing spaces in semantics_tm. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  40. No space in front of object-logic forall. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  41. Non-conflicting name for boolean denotation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  42. Simpler Hintikka definition. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  43. Add syntactic abbreviation for constants. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  44. Add papers to metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  45. In the definition of regular pair, switched from strict to non-strict — paulson <lp15@cam.ac.uk> / hgweb
  46. A slightly stronger lemma allowing slightly simpler proofs — paulson <lp15@cam.ac.uk> / hgweb

#82 (Dec 12, 2021, 12:14:00 AM)

  1. provide component naproche-20211211; — wenzelm / hgweb
  2. merged — wenzelm / hgweb
  3. more Mailman archives; — wenzelm / hgweb
  4. more Mailman content; — wenzelm / hgweb
  5. clarified signature; — wenzelm / hgweb
  6. tuned metis to use map_index — desharna / hgweb
  7. merged — desharna / hgweb
  8. fixed HOL-TPTP — desharna / hgweb
  9. tuned vars_of_iterm — desharna / hgweb
  10. fixed TPTP generation of multi-arity expressions — desharna / hgweb
  11. proper handling of Hilbert choice in TFX logics — desharna / hgweb
  12. proper tptp_builtins — desharna / hgweb
  13. reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle — desharna / hgweb
  14. proper proxy for Hilbert choice in TPTP output — desharna / hgweb
  15. proper polymorphism for TH1 format in Sledgehammer — desharna / hgweb
  16. refactored $ite and $let configuration and added dummy_thf_reduced prover — desharna / hgweb
  17. tuned TPTP file names generated by Sledgehammer — desharna / hgweb
  18. tuned SMT-Lib file names generated by Mirabelle — desharna / hgweb
  19. added support for higher-order SMT proof search in Sledgehammer — desharna / hgweb
  20. separated FOOL from $ite/$let in TPTP output — desharna / hgweb
  21. missing latex font — nipkow / hgweb
  22. Rewrite: added links to docu, made more prominent — nipkow / hgweb
  23. discontinued old-style {* verbatim *} tokens; — wenzelm / hgweb
  24. tuned proof; — wenzelm / hgweb
  25. isabelle update_cartouches; — wenzelm / hgweb
  26. more symbolic latex_output via XML (using YXML within text); — wenzelm / hgweb
  27. tuned signature: remove unused; — wenzelm / hgweb
  28. prefer symbolic Latex.environment (typeset in Isabelle/Scala); — wenzelm / hgweb
  29. tuned signature; — wenzelm / hgweb
  30. clarified corner cases of syntax; — wenzelm / hgweb
  31. clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2); — wenzelm / hgweb
  32. a slightly simpler proof — paulson <lp15@cam.ac.uk> / hgweb

#82 (Dec 12, 2021, 12:14:00 AM)

  1. merged — desharna / hgweb
  2. generalized standard formula redundancy out of standard redundancy — desharna / hgweb
  3. merged — wenzelm / hgweb
  4. discontinued Parse.text; — wenzelm / hgweb
  5. discontinued old-style {* verbatim *} tokens; — wenzelm / hgweb
  6. weakened locale assumptions: wfP implies asymp — desharna / hgweb
  7. Add papers to metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  8. refactored Standard_Redundancy_Criterion to not use ordering type classes — desharna / hgweb
  9. isabelle update_cartouches; — wenzelm / hgweb
  10. removed obsolete "extend" operation; — wenzelm / hgweb
  11. more symbolic latex_output via XML (using YXML within text);
    re-use existing Latex.output_markup; — wenzelm / hgweb
  12. prefer symbolic Latex.environment (typeset in Isabelle/Scala); — wenzelm / hgweb
  13. tuned signature; — wenzelm / hgweb

#81 (Dec 5, 2021, 12:14:00 AM)

  1. provide component naproche-2d99afe5c349; — wenzelm / hgweb
  2. merged — wenzelm / hgweb
  3. Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2 — wenzelm / hgweb
  4. more documentation about Type/Const antiquotations; — wenzelm / hgweb
  5. more documentation about document build options; — wenzelm / hgweb
  6. address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c); — wenzelm / hgweb
  7. tuned --- fewer IDE warnings; — wenzelm / hgweb
  8. more robust physical timeout (despite 1bea05713dde), especially relevant for quickcheck where large unary numerals may cause excessive heap allocations and resulting GC is better included in the timing; — wenzelm / hgweb
  9. added definitions multp{DM,HO} and corresponding lemmas — desharna / hgweb
  10. added wfP_less to wellorder and wfP_less_multiset — desharna / hgweb
  11. restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3 — desharna / hgweb
  12. merged — desharna / hgweb
  13. added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset — desharna / hgweb
  14. redefined less_multiset to be based on multp — desharna / hgweb
  15. added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp — desharna / hgweb
  16. added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max — desharna / hgweb
  17. added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp — desharna / hgweb
  18. added lemma wfP_multp — desharna / hgweb
  19. added lemma mono_multp — desharna / hgweb
  20. added Multiset.multp as predicate equivalent of Multiset.mult — desharna / hgweb
  21. address problems with launch4j and jdk-17 (see also 41d009462d3c); — wenzelm / hgweb
  22. more robust build on midrange hardware; — wenzelm / hgweb
  23. clarified tests: omit somewhat pointless (unstable) results; — wenzelm / hgweb
  24. proper fields for gnuplot (amending b614e3e4146a); — wenzelm / hgweb
  25. tuned output; — wenzelm / hgweb
  26. tuned; — wenzelm / hgweb
  27. merged — wenzelm / hgweb
  28. more robust build on midrange hardware (despite 67d6f1708ea4); — wenzelm / hgweb
  29. Added tag Isabelle2021-1-RC4 for changeset 2336356d4180 — wenzelm / hgweb
  30. updated to polyml-5.9; — wenzelm / hgweb
  31. NEWS on "isabelle mirabelle"; — wenzelm / hgweb
  32. tuned; — wenzelm / hgweb
  33. clarified default for kodkod_scala;
    NEWS for proper release; — wenzelm / hgweb
  34. maintain option kodkod_scala within theory context, to allow local modification; — wenzelm / hgweb
  35. NEWS for proper release; — wenzelm / hgweb
  36. updated to flatlaf-1.6.4; — wenzelm / hgweb
  37. avoid broken links: auxiliary files are not yet supported; — wenzelm / hgweb
  38. option document_comment_latex supports e.g. Dagstuhl LIPIcs; — wenzelm / hgweb
  39. more explicit type Latex.Tags;
    generate isabelletags.sty from Isabelle/Scala, including comment.sty setup; — wenzelm / hgweb
  40. more uniform treatment of optional_argument for Latex elements;
    discontinued somewhat pointless element position in Isabelle/Scala: semantic add-ons are better provided in Isabelle/ML;
    clarified signature of class Latex: overridable unknown_elem allows to extend the markup language; — wenzelm / hgweb
  41. removed pointless 'text_cartouche' command: regular 'text' already supports cartouches; — wenzelm / hgweb
  42. example: alternative document headings, based on more general document output markup; — wenzelm / hgweb
  43. more general document output: enclosing markup is defined in user-space; — wenzelm / hgweb
  44. clarified modules (see c299abcf7081); — wenzelm / hgweb
  45. output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction; — wenzelm / hgweb
  46. clarified modules; — wenzelm / hgweb
  47. tuned signature: more explicit types for presentation; — wenzelm / hgweb
  48. more robust support for Windows line-endings; — wenzelm / hgweb
  49. source positions for document markup commands, e.g. to retrieve PIDE markup in presentation; — wenzelm / hgweb
  50. more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory; — wenzelm / hgweb
  51. clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true"; — wenzelm / hgweb
  52. more symbolic latex_output via XML (using YXML within text); — wenzelm / hgweb
  53. proper enclose_name (amending e77c5bfca9aa); — wenzelm / hgweb
  54. Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.; — wenzelm / hgweb
  55. more symbolic latex_output via XML; — wenzelm / hgweb
  56. clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab); — wenzelm / hgweb
  57. tuned; — wenzelm / hgweb
  58. tuned; — wenzelm / hgweb
  59. updated to verit-2021.06.2-rmx; — wenzelm / hgweb
  60. clarified HTML_Context.theory_exports: prefer value-oriented parallelism; — wenzelm / hgweb
  61. generate problems with correct logic for veriT — fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
  62. more parallelism, at the cost of potential duplicates of make_thy; — wenzelm / hgweb
  63. afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a); — wenzelm / hgweb
  64. more interrupts; — wenzelm / hgweb
  65. present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826;
    eliminated implicit state: these theories are globally unique; — wenzelm / hgweb
  66. tuned; — wenzelm / hgweb
  67. clarified modules; — wenzelm / hgweb
  68. tuned (see also e0d1d9203275); — wenzelm / hgweb
  69. clarified signature; — wenzelm / hgweb
  70. tuned; — wenzelm / hgweb
  71. spelling; — wenzelm / hgweb

#81 (Dec 5, 2021, 12:14:00 AM)

  1. feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics and multiple times — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  2. Tuned: use a star in witness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  3. merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  4. adjust for new tags in Isabelle2021-1-RC4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  5. fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb
  6. In the definition of regular pair, switched from strict to non-strict — paulson <lp15@cam.ac.uk> / hgweb
  7. Rename H to S in maximal_exactly_one. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  8. Get rid of the sat abbreviation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  9. Add missing spaces in semantics_tm. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  10. No space in front of object-logic forall. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  11. Non-conflicting name for boolean denotation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  12. Simpler Hintikka definition. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  13. Add syntactic abbreviation for constants. — Asta Halkjær From <andro.from@gmail.com> / hgweb
  14. fixed lemma following Isabelle/c256bba593f3 — desharna / hgweb
  15. fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb

#80 (Nov 28, 2021, 12:14:00 AM)

  1. added asymp_{less,greater} to preorder and moved mult1_lessE out — desharna / hgweb
  2. renamed multp_code_iff and multeqp_code_iff — desharna / hgweb
  3. simplified mult_cancel_max and introduced orginal lemma as mult_cancel_max0 — desharna / hgweb
  4. renamed Multiset.multp and Multiset.multeqp — desharna / hgweb

#79 (Nov 21, 2021, 12:14:00 AM)

  1. added lemmas — nipkow / hgweb
  2. merged — wenzelm / hgweb
  3. tuned; — wenzelm / hgweb
  4. removed redundant test (see also 86fac52c2795, a9fea3f11cc0); — wenzelm / hgweb
  5. just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow); — wenzelm / hgweb
  6. proper version; — wenzelm / hgweb
  7. back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in Padic_Ints (AFP/7a2522dce834); — wenzelm / hgweb
  8. less ambitious parallelism: more direct read/write saves overall heap space and GC time; — wenzelm / hgweb
  9. slightly faster XML output: avoid too much regrowing of StringBuilder; — wenzelm / hgweb
  10. updated NEWS: arm64-linux support is almost complete; — wenzelm / hgweb
  11. update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9; — wenzelm / hgweb
  12. more material for HOL-Analysis.Infinite_Sum — Manuel Eberl <manuel@pruvisto.org> / hgweb
  13. more symbolic latex_output via XML; — wenzelm / hgweb
  14. clarified signature; — wenzelm / hgweb
  15. updated to polyml-5.9-610a153b941d -- close to final; — wenzelm / hgweb
  16. tuned signature (again): latex_output is likely to depend on context; — wenzelm / hgweb
  17. more symbolic latex output;
    discontinued Latex.output_text, which is in conflict with symbolic output; — wenzelm / hgweb
  18. tuned signature; — wenzelm / hgweb
  19. symbolic latex_output via XML, interpreted in Isabelle/Scala; — wenzelm / hgweb
  20. tuned signature; — wenzelm / hgweb
  21. clarified signature; — wenzelm / hgweb
  22. clarified signature; — wenzelm / hgweb
  23. clarified signature: more privacy; — wenzelm / hgweb
  24. tuned output --- less redundancy; — wenzelm / hgweb
  25. tuned whitespace; — wenzelm / hgweb
  26. clarified signature: Latex.Output as parameter to Document_Build.Engine;
    tuned; — wenzelm / hgweb
  27. proper detection of ARM platform variants; — wenzelm / hgweb
  28. back to post-release mode; — wenzelm / hgweb
  29. updated for release; — wenzelm / hgweb
  30. Added tag Isabelle2021-1-RC3 for changeset 2b212c8138a5 — wenzelm / hgweb
  31. merged — wenzelm / hgweb
  32. updated to polyml-5.9-cc80e2b43c38, which also contains ARM64 on darwin (unused by default); — wenzelm / hgweb
  33. clarified HTML_Context: more explicit directory structure; — wenzelm / hgweb
  34. tuned comments; — wenzelm / hgweb
  35. tuned; — wenzelm / hgweb
  36. clarified signature; — wenzelm / hgweb
  37. clarified properties: avoid empty entry; — wenzelm / hgweb
  38. tuned signature; — wenzelm / hgweb

#79 (Nov 21, 2021, 12:14:00 AM)

  1. A slightly stronger lemma allowing slightly simpler proofs — paulson <lp15@cam.ac.uk> / hgweb
  2. Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now in Isabelle itself — Dominique Unruh <unruh@ut.ee> / hgweb
  3. Elimination of all z3 calls — paulson <lp15@cam.ac.uk> / hgweb
  4. Word_Lib sync from l4v; tweak word_eqI — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  5. generalise word_eqI method; make sure it is exercised — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  6. test_bit_size not longer needed; avoid potential nontermination — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  7. Word_Lib tweaks for slightly more backwards compatibility — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  8. use bit_simps in word_eqI method — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  9. adapted to new version of Infinite_Sum in isabelle-dev — Manuel Eberl <eberlm@in.tum.de> / hgweb
  10. avoid hardwired document output; — wenzelm / hgweb
  11. CTR and ETTS: integration with SpecCheck: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
  12. Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL-Analysis.Infinite_Sum — Dominique Unruh <unruh@ut.ee> / hgweb
  13. Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum — Dominique Unruh <unruh@ut.ee> / hgweb
  14. merge — Burkhart Wolff <wolff@lri.fr> / hgweb
  15. merge — Burkhart Wolff <wolff@lri.fr> / hgweb
  16. Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc. — Burkhart Wolff <wolff@lri.fr> / hgweb
  17. documentation fine-tuning. — Burkhart Wolff <wolff@lri.fr> / hgweb
  18. Added section on C11_Ast_Lib in chapter II. — Burkhart Wolff <wolff@lri.fr> / hgweb
  19. Example section restored and Documentation adapted. — Burkhart Wolff <wolff@lri.fr> / hgweb
  20. Stramge intermediate configuration: Example section zerschossen. — Burkhart Wolff <wolff@lri.fr> / hgweb
  21. Port to Isabelle2021-1 RC 2. — Burkhart Wolff <wolff@lri.fr> / hgweb
  22. Improved documentation. — Burkhart Wolff <wolff@lri.fr> / hgweb
  23. Examples for  iterator - applications: queries,  and translations into term. — Burkhart Wolff <wolff@lri.fr> / hgweb
  24. Rearranging standard root store; better documentation in C_Command. — Burkhart Wolff <wolff@lri.fr> / hgweb
  25. Rearranging the ML _programming Example Section C1. — Burkhart Wolff <wolff@lri.fr> / hgweb
  26. reorg 1 — Burkhart Wolff <wolff@lri.fr> / hgweb
  27. ... — Burkhart Wolff <wolff@lri.fr> / hgweb
  28. Improved Standard Interface to C11: Better signatures, a CEnv signature, C11 Std Ast Store (in C2.thy) — Burkhart Wolff <wolff@lri.fr> / hgweb
  29. Restructuring of Interfaces; more show cases. — Burkhart Wolff <wolff@lri.fr> / hgweb
  30. Updated meta-data for Optics — Simon Foster <simon.foster@york.ac.uk> / hgweb
  31. Additional scene laws — Simon Foster <simon.foster@york.ac.uk> / hgweb
  32. Branch merge — Simon Foster <simon.foster@york.ac.uk> / hgweb
  33. Improved support for code generation, fixed a few bugs, and added a tactic to aid proof goal presentation of lens variables. — Simon Foster <simon.foster@york.ac.uk> / hgweb
  34. feat(SpecCheck/Show) add parentheses for option SOME case — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  35. merged — desharna / hgweb
  36. weakened ordering requirements — desharna / hgweb
  37. used well-founded pre-order in standard redundancy criterions — desharna / hgweb
  38. derived refutational completeness from finitary and non-finitary standard redundancy criterion — desharna / hgweb
  39. merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  40. deleted incomplete methods for polynomial factorization or root computation in Algebraic-Numbers, since
    they are now available as complete methods in Factor-Algebraic-Polynomial — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  41. factor_complex_poly delivers distinct list — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  42. merged — paulson / hgweb
  43. Removal of material that's going to be in Isabelle2021-1 — paulson <lp15@cam.ac.uk> / hgweb
  44. merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  45. refactoring (moving theories and lemmas around) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  46. sync from l4v — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  47. adjusted Factor_Algebraic_Polynomial to Isabelle/devel (and Isabelle 2021-1, RC3) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  48. merge of afp-2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  49. new entry PAL — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  50. new entry Factor_Algebraic_Polynomial — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  51. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  52. document `publish -` — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  53. changed affiliation of eberl (this time properly) — Manuel Eberl <manuel@pruvisto.org> / hgweb
  54. changed affiliation of Eberl — Manuel Eberl <manuel@pruvisto.org> / hgweb
  55. sitegen for Real_Power — paulson <lp15@cam.ac.uk> / hgweb
  56. new entry Real_Power — paulson <lp15@cam.ac.uk> / hgweb
  57. New entry Szemeredi_Regularity — nipkow / hgweb
  58. tuned proofs -- avoid z3; — wenzelm / hgweb

#78 (Nov 14, 2021, 12:14:00 AM)

  1. merged — nipkow / hgweb
  2. tuned (thanks to J. Villadsen) — nipkow / hgweb
  3. added padding to Mirabelle's output — desharna / hgweb
  4. merged — desharna / hgweb
  5. tuned generation of TPTP with $ite/$let in higher-order logics — desharna / hgweb
  6. tuned generation of TPTP with $ite in function position — desharna / hgweb
  7. tuned TPTP generation of If helper facts — desharna / hgweb
  8. merged — wenzelm / hgweb
  9. clarified signature: prefer static operations; — wenzelm / hgweb
  10. clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources; — wenzelm / hgweb
  11. more robust; — wenzelm / hgweb
  12. tuned signature; — wenzelm / hgweb
  13. clarified signature: more explicit class Entity_Context with private state + operations; — wenzelm / hgweb
  14. more hyperlinks, notably internal fact references; — wenzelm / hgweb
  15. Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO — paulson <lp15@cam.ac.uk> / hgweb
  16. A tiny bit of tidying connected with Zorn's Lemma — paulson <lp15@cam.ac.uk> / hgweb
  17. tuned; — wenzelm / hgweb
  18. tuned; — wenzelm / hgweb
  19. proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition); — wenzelm / hgweb
  20. revert temporary workaround 6d111935299c; — wenzelm / hgweb
  21. added lemma — nipkow / hgweb
  22. merged — nipkow / hgweb
  23. tuned attributes to avoid looping — nipkow / hgweb
  24. added eq_iff_swap for creating symmetric variants of thms; applied it in List. — nipkow / hgweb
  25. tuned text; — wenzelm / hgweb
  26. more robust timeout, following df4449c6eff1; — wenzelm / hgweb
  27. more accurate Files.isRegularFile, exclude directories (e.g. jar_path); — wenzelm / hgweb
  28. proper java_version for isabelle_setup; — wenzelm / hgweb
  29. explicit option metric_argo_timeout, with reasonable default for Raspberry Pi; — wenzelm / hgweb
  30. tuned; — wenzelm / hgweb
  31. repackage minisat-2.2.1 with cygwin1.dll: required to run the executable without existing Cygwin context (normally provided by bash_process); — wenzelm / hgweb
  32. discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do; — wenzelm / hgweb
  33. clarified messages, depending on option "document_echo"; — wenzelm / hgweb
  34. just one cache, via HTML_Context, via Sessions.Store or Session; — wenzelm / hgweb
  35. merged — paulson / hgweb
  36. new lemmas about convex, concave functions, + tidying — paulson <lp15@cam.ac.uk> / hgweb
  37. proper support for arm64; — wenzelm / hgweb
  38. no perl (amending 59ef23ac81ab); — wenzelm / hgweb
  39. merged — wenzelm / hgweb
  40. Added tag Isabelle2021-1-RC2 for changeset b92b5a57521b — wenzelm / hgweb
  41. merged — nipkow / hgweb
  42. Preserve variable name z in VAR {z = t} — nipkow / hgweb
  43. back to scala-2.13.5: avoid crash of Scala REPL on arm64-darwin; — wenzelm / hgweb
  44. updated to polyml-5.9-5d4caa8f7148, which also contains ARM64 on darwin (unused by default); — wenzelm / hgweb
  45. more precise URL — nipkow / hgweb
  46. tuned page breaks — nipkow / hgweb

#78 (Nov 14, 2021, 12:14:00 AM)

  1. CTR and ETTS: integration with SpecCheck — user9716869 <user9716869@gmail.com> / hgweb
  2. used antiquotation to fix LaTeX failure — desharna / hgweb
  3. adapted to devel — nipkow / hgweb
  4. updated to devel — nipkow / hgweb
  5. merged — nipkow / hgweb
  6. tuned proof for devel — nipkow / hgweb
  7. clarified quotes vs. apostrophes vs. primes; — wenzelm / hgweb
  8. more accurate use of LaTeX ndash; — wenzelm / hgweb
  9. prefer portable LaTeX mdash; — wenzelm / hgweb
  10. tuned whitespace --- removed suspicious Unicode; — wenzelm / hgweb
  11. proper Unix linefeeds; — wenzelm / hgweb
  12. changed affiliation of eberl (this time properly) — Manuel Eberl <manuel@pruvisto.org> / hgweb
  13. changed affiliation of eberl — Manuel Eberl <manuel@pruvisto.org> / hgweb
  14. added author to Saturation_Framework_Extensions — desharna / hgweb
  15. derived calculus_with_standard_redundancy lemmas from calculus_with_finitary_standard_redundancy — desharna / hgweb
  16. added locale calculus_with_finitary_standard_redundancy — desharna / hgweb
  17. Registers:
    - Added mechanism for raising errors if autogenerated files need updating
    - Changed definition of Axioms_Quantum.register_pair (returns 0 for incompatible registers, see register_pair_is_register_converse for a useful consequence)
    - Slightly reducing namespace pollution in Classical_Extra (hiding consts x, y, X, Y etc.) — Dominique Unruh <unruh@ut.ee> / hgweb
  18. feat(SpecCheck) add better unit tests facilities, examples and exceptions property — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  19. discontinued somewhat pointless and slightly outdated document_preprocessor (after consultation with the author); — wenzelm / hgweb
  20. Correctness_Algebras: increase nitpick timeout — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  21. CZH: dagger monoidal categories — user9716869 <user9716869@gmail.com> / hgweb
  22. update it Isabelle/925b46043b84 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  23. merge from afp-2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  24. sitegen for Registers — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  25. new entry Registers — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb

#77 (Nov 7, 2021, 12:14:00 AM)

  1. cover all possible kinds, notably for references outside of this theory (amending 129fb11b357f); — wenzelm / hgweb
  2. proper foundational order; — wenzelm / hgweb
  3. back to non-strict Export_Theory.read_theory (without warning): theories could have been skipped due to "condition"; — wenzelm / hgweb
  4. use all entity kinds from theory export, e.g. "method", "attribute"; — wenzelm / hgweb
  5. clarified signature; — wenzelm / hgweb
  6. clarified physical_ref; — wenzelm / hgweb
  7. proper treatment of session build hierarchy; — wenzelm / hgweb
  8. proper used_theories for session build hierarchy, not known_theories from imported sessions; — wenzelm / hgweb
  9. present theories from imported sessions as required; — wenzelm / hgweb
  10. avoid multiple copies of fonts;
    proper fonts prefix for aux. files; — wenzelm / hgweb
  11. more compact persistent data; — wenzelm / hgweb
  12. tuned; — wenzelm / hgweb
  13. proper term_cache; — wenzelm / hgweb
  14. prefer "NAME|KIND" format, as already used in Isabelle/MMT and Isabelle/Dedukti; — wenzelm / hgweb
  15. tuned; — wenzelm / hgweb
  16. observer proper session hierarchy (according to build_graph): thus exported artifacts are always valid; — wenzelm / hgweb
  17. tuned; — wenzelm / hgweb
  18. clarified order: prefer bottom-up construction of partial content; — wenzelm / hgweb
  19. more thorough update_global_index: overwrite old content; — wenzelm / hgweb
  20. tuned; — wenzelm / hgweb
  21. tuned; — wenzelm / hgweb
  22. clarified HTML_Context: just one context type; — wenzelm / hgweb
  23. unused (see also 217e6cf61453, 5e7916535860); — wenzelm / hgweb
  24. merged — wenzelm / hgweb
  25. clarified Theory_Cache: prefer immutable data with Synchronized variable;
    clarified Export_Theory.Theory vs. Entity tables;
    entity_ref: proper treatment of entity kind; — wenzelm / hgweb
  26. tuned signature; — wenzelm / hgweb
  27. unused; — wenzelm / hgweb
  28. proper support of verit's return code for timeout — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
  29. tuned whitespace; — wenzelm / hgweb
  30. updated to verit-2021.06.1-rmx, to address "Abnormal termination with exit code 14"; — wenzelm / hgweb
  31. clarified signature; — wenzelm / hgweb
  32. prefer official Export.explode_name;
    avoid string interpolation: Isabelle/Scala is closer to Isabelle/ML than Python/Perl; — wenzelm / hgweb
  33. tuned; — wenzelm / hgweb
  34. avoid conflict with future keyword; — wenzelm / hgweb
  35. tuned messages; — wenzelm / hgweb
  36. clarified signature: more direct XML.symbol_length; — wenzelm / hgweb
  37. more direct Symbol.length: Symbol.decode is redundant, symbol counts are invariant under it; — wenzelm / hgweb
  38. tuned -- eliminate clones stemming from d28a51dd9da6; — wenzelm / hgweb
  39. more to ANNOUNCE; — wenzelm / hgweb
  40. clarified link style: similar to Isabelle/jEdit; — wenzelm / hgweb
  41. tuned; — wenzelm / hgweb
  42. improved HTML presentation by Fabian Huch; — wenzelm / hgweb
  43. proper HTTPS; — wenzelm / hgweb
  44. proper markup type (amending be49c660ebbf); — wenzelm / hgweb
  45. merged; — wenzelm / hgweb
  46. more PIDE markup; — wenzelm / hgweb
  47. tuned signature; — wenzelm / hgweb
  48. more PIDE markup; — wenzelm / hgweb
  49. recover library_index_content.template from c337c798f64c: required for website/build/main; — wenzelm / hgweb
  50. merged — paulson / hgweb
  51. simplified some ugly proofs — paulson <lp15@cam.ac.uk> / hgweb
  52. more generous timeout: support build on Raspberry Pi; — wenzelm / hgweb
  53. add documentation for pred_mono — traytel / hgweb
  54. merged — desharna / hgweb
  55. added "mono" attribute to BNF generated pred_mono theorems — desharna / hgweb
  56. merged — desharna / hgweb
  57. do not declare $let-bound variables in TPTP output — desharna / hgweb
  58. IDE build actually works (but somewhat pointless); — wenzelm / hgweb
  59. suppress sources from jEdit/test, which prevent regular build of the generated scala_project; — wenzelm / hgweb
  60. removed junk; — wenzelm / hgweb
  61. improve pagebreaks by *not* using supertabular too much; — wenzelm / hgweb
  62. updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc; — wenzelm / hgweb
  63. more robust "isabelle scala_project": Gradle has been replaced by Maven; — wenzelm / hgweb
  64. tuned; — wenzelm / hgweb
  65. support linux_arm as well, e.g. native Docker on Apple Silicon; — wenzelm / hgweb
  66. update paths at TUM; — wenzelm / hgweb
  67. Added tag Isabelle2021-1-RC1 for changeset 81cc8f2ea9e7 — wenzelm / hgweb
  68. updated for release; — wenzelm / hgweb
  69. some reordering for release; — wenzelm / hgweb
  70. updated to jdk-17.0.1+12; — wenzelm / hgweb
  71. tuned message; — wenzelm / hgweb
  72. clarified antiquotations; — wenzelm / hgweb
  73. tuned; — wenzelm / hgweb
  74. minor performance tuning; — wenzelm / hgweb
  75. more robust; — wenzelm / hgweb
  76. provide native executables for arm64-darwin, for more robust startup without Rosetta 2; — wenzelm / hgweb
  77. tuned proofs -- avoid z3, which is unavailable on arm64-linux; — wenzelm / hgweb
  78. prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms; — wenzelm / hgweb
  79. discontinued pointless check of kodkodi_version, it is implicit in the bundled component; — wenzelm / hgweb

#77 (Nov 7, 2021, 12:14:00 AM)

  1. Correctness_Algebras: increase session timeout — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  2. tuned signature, according to Isabelle/df12779c3ce8; — wenzelm / hgweb
  3. feat(SpecCheck) add possibility to make builds fail on failure and extend README — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  4. added missing funding information — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  5. restored theory structure for simple genericity. — haftmann / hgweb
  6. Backed out changeset af549be0a8cd — haftmann / hgweb
  7. restored different entrance points a before Isabelle2021 — haftmann / hgweb
  8. proper parentheses (amending 354560d7143a); — wenzelm / hgweb
  9. Adjusted to prospective release Isabelle2021-2. — haftmann / hgweb
  10. Correctness_Algebras: uncomment counterexamples — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  11. clarified identity of theory data: avoid accidental pointer_eq, use equality on unique serial instead; — wenzelm / hgweb
  12. clarified identity of theory data: pointer_eq is not well-defined (and fails on ARM64), use equality on unique serial instead; — wenzelm / hgweb
  13. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  14. remove unused functions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  15. silence sitegen warning — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  16. new entry X86_Semantics — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  17. adjust to isabelle@549019b4a808 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  18. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  19. metadata for Belief_Revision — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  20. new entry Belief_Revision — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  21. New entry Correctness_Algebras — nipkow / hgweb
  22. prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms; — wenzelm / hgweb

#76 (Oct 31, 2021, 12:14:00 AM)

  1. tuned proofs -- avoid z3, which is unavailable on arm64-linux; — wenzelm / hgweb
  2. tuned; — wenzelm / hgweb
  3. test version of prespective polyml-5.9; — wenzelm / hgweb
  4. clarified antiquotations; — wenzelm / hgweb
  5. updated for pre-5.9 testing; — wenzelm / hgweb
  6. clarified antiquotations; — wenzelm / hgweb
  7. clarified antiquotations; — wenzelm / hgweb
  8. clarified antiquotations; — wenzelm / hgweb
  9. more robust subgoal addressing; — wenzelm / hgweb
  10. proper subgoal addressing; — wenzelm / hgweb
  11. clarified antiquotations; — wenzelm / hgweb
  12. recursive find_eq, not find_dist; — wenzelm / hgweb
  13. misc tuning and clarification; — wenzelm / hgweb
  14. clarified antiquotations; — wenzelm / hgweb
  15. order_tac: prevent potential bug, improve perf and tracing

    - We need to be careful when the order operators contain schematic variables, e.g. <= = ccw' ?p. — Lukas Stevens <mail@lukas-stevens.de> / hgweb
  16. misc tuning and clarification; — wenzelm / hgweb
  17. clarified antiquotations; — wenzelm / hgweb
  18. clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta; — wenzelm / hgweb
  19. clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta; — wenzelm / hgweb
  20. avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570); — wenzelm / hgweb
  21. added Thm.instantiate_beta;
    tuned; — wenzelm / hgweb
  22. moved generic implementation into HOL-Main — haftmann / hgweb
  23. tuned; — wenzelm / hgweb
  24. tuned; — wenzelm / hgweb
  25. clarified antiquotations; — wenzelm / hgweb
  26. clarified antiquotations; — wenzelm / hgweb
  27. discontinued somewhat pointless antiquotations; — wenzelm / hgweb
  28. NEWS; — wenzelm / hgweb
  29. clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic; — wenzelm / hgweb
  30. clarified antiquotations; — wenzelm / hgweb
  31. clarified antiquotations; — wenzelm / hgweb
  32. clarified antiquotations; — wenzelm / hgweb
  33. clarified antiquotations; — wenzelm / hgweb
  34. support for "lemma";
    support for "schematic" mode;
    clarified error position; — wenzelm / hgweb
  35. tuned; — wenzelm / hgweb
  36. local fixes for "lemma" antiquotation; — wenzelm / hgweb
  37. clarified signature; — wenzelm / hgweb
  38. tuned; — wenzelm / hgweb
  39. clarified keywords: major take precedence for commands, but not used for antiquotations;
    clarified modules; — wenzelm / hgweb
  40. tuned modules; — wenzelm / hgweb
  41. more antiquotations; — wenzelm / hgweb
  42. moved a theorem to a sensible place — paulson <lp15@cam.ac.uk> / hgweb
  43. merged — wenzelm / hgweb
  44. tuned, continuing e955964d89cb; — wenzelm / hgweb
  45. avoid waste of resources due to dynamic simpset (amending 45c09620f726); — wenzelm / hgweb
  46. fix latex — Norbert Schirmer <nschirmer@apple.com> / hgweb
  47. clarified modules; — wenzelm / hgweb
  48. more generic bit/word lemmas for distribution — haftmann / hgweb
  49. merged — paulson / hgweb
  50. Added / moved some simple set-theoretic lemmas — paulson <lp15@cam.ac.uk> / hgweb
  51. more CONTRIBUTORS and NEWS; — wenzelm / hgweb
  52. cleanup; add Apple reference — Norbert Schirmer <nschirmer@apple.com> / hgweb
  53. refine interface — Norbert Schirmer <nschirmer@apple.com> / hgweb
  54. generalized component lookup for syntax and distinctness proofs. added some tracing. — Norbert Schirmer <nschirmer@apple.com> / hgweb
  55. merged — wenzelm / hgweb
  56. tuned; — wenzelm / hgweb
  57. more antiquotations; — wenzelm / hgweb
  58. more antiquotations; — wenzelm / hgweb
  59. more robust: genuinely free variables need to be instantiated; — wenzelm / hgweb
  60. tuned comments; — wenzelm / hgweb
  61. clarified errors; — wenzelm / hgweb
  62. tuned; — wenzelm / hgweb
  63. clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs; — wenzelm / hgweb
  64. tuned; — wenzelm / hgweb
  65. clarified signature -- avoid clones; — wenzelm / hgweb
  66. Refinement of partitions — paulson <lp15@cam.ac.uk> / hgweb
  67. avoid persistence of static context: instantiation arguments should provide proper dynamic context; — wenzelm / hgweb
  68. more antiquotations; — wenzelm / hgweb
  69. more markup; — wenzelm / hgweb
  70. clarified name, syntax, messages; — wenzelm / hgweb
  71. more antiquotations; — wenzelm / hgweb
  72. more control symbols; — wenzelm / hgweb
  73. tuned signature; — wenzelm / hgweb
  74. ML antiquotations to instantiate types/terms/props; — wenzelm / hgweb
  75. tuned; — wenzelm / hgweb
  76. clarified modules; — wenzelm / hgweb
  77. clarified modules; — wenzelm / hgweb
  78. clarified modules; — wenzelm / hgweb
  79. discontinued obsolete "val extend = I" for data slots; — wenzelm / hgweb
  80. clarified modules; — wenzelm / hgweb
  81. clarified modules; — wenzelm / hgweb
  82. clarified signature; — wenzelm / hgweb
  83. tuned; — wenzelm / hgweb
  84. clarified keywords and reports; — wenzelm / hgweb
  85. clarified signature; — wenzelm / hgweb
  86. merged — desharna / hgweb
  87. proper veriT --max-time option — desharna / hgweb
  88. refactored tptp_builtins in Sledgehammer — desharna / hgweb
  89. merged — wenzelm / hgweb
  90. tuned ML --- clarified use of context;
    tuned message; — wenzelm / hgweb
  91. tuned --- fewer clones; — wenzelm / hgweb
  92. updated to jEdit plugin Highlight 2.5; — wenzelm / hgweb
  93. proper tactic combinator; — wenzelm / hgweb
  94. proper file headers; — wenzelm / hgweb
  95. clarified context;
    clarified modules; — wenzelm / hgweb
  96. more accurate treatment of context; — wenzelm / hgweb
  97. updated email address — Manuel Eberl <manuel@pruvisto.org> / hgweb
  98. removed some 'private' modifiers from HOL-Computational_Algebra — Manuel Eberl <manuel@pruvisto.org> / hgweb
  99. merged — wenzelm / hgweb
  100. merged — wenzelm / hgweb
  101. more robust Variable.revert_bounds (see also b12f2cef3ee5); — wenzelm / hgweb
  102. more accurate treatment of context; — wenzelm / hgweb
  103. tuned -- proper names/scopes for contexts; — wenzelm / hgweb
  104. clarified context; — wenzelm / hgweb
  105. clarified context; — wenzelm / hgweb
  106. tuned; — wenzelm / hgweb
  107. unused; — wenzelm / hgweb
  108. more accurate treatment of context;
    declare generated bounds for the sake of recdef, which has variables leaking from local context; — wenzelm / hgweb
  109. isabelle regenerate_cooper; — wenzelm / hgweb
  110. revert bbfed17243af, breaks HOL-Proofs extraction; — wenzelm / hgweb
  111. tuned; — wenzelm / hgweb
  112. tuned; — wenzelm / hgweb
  113. proper p' instead of p (amending 52c7c42e7e27); — wenzelm / hgweb
  114. proper context for Goal.prove_internal; — wenzelm / hgweb
  115. discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
    Simplifier and equational conversions demand a proper proof context; — wenzelm / hgweb
  116. more accurate treatment of context, notably for nested Goal.proof / SUBPROOF; — wenzelm / hgweb
  117. tuned; — wenzelm / hgweb
  118. tuned; — wenzelm / hgweb
  119. tuned; — wenzelm / hgweb
  120. spelling; — wenzelm / hgweb
  121. clarified context; — wenzelm / hgweb
  122. clarified signature; — wenzelm / hgweb
  123. tuned Vampire configuration to use TFX in Sledgehammer — desharna / hgweb

#76 (Oct 31, 2021, 12:14:00 AM)

  1. updated metadata for Count_Complex_Roots — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
  2. corrected the timeout for CZH_Universal_Constructions — user9716869 <user9716869@gmail.com> / hgweb
  3. CZH: further results about comma categories and Kan extensions, a variety of other minor amendments — user9716869 <user9716869@gmail.com> / hgweb
  4. more generic bit/word lemmas for distribution — haftmann / hgweb
  5. Fixing a name clash between two different "restrict" operators — paulson <lp15@cam.ac.uk> / hgweb
  6. Merged — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
  7. solved the roots-on-the-border problem — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
  8. split Count_Complex_Roots — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
  9. more realistic timeout; — wenzelm / hgweb
  10. clarified signature, according to Isabelle/ccf599864beb; — wenzelm / hgweb
  11. back to dedicated separate shift operations for infix syntax;
    more default simp rules on closed numeric expressions — haftmann / hgweb
  12. modify JinjaDCI — nanjiang <nanjiang@whu.edu.cn> / hgweb
  13. modify JinjaDCI — nanjiang <nanjiang@whu.edu.cn> / hgweb
  14. Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  15. Various tuning that for some reason didn't get merged from my master branch. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  16. A spot of polishing — paulson <lp15@cam.ac.uk> / hgweb
  17. Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  18. Update metadata to reflect changes made in July, 2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  19. Add a revision note concerning material added in July, 2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  20. tuned signature, according to Isabelle/042041c0ebeb; — wenzelm / hgweb
  21. Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  22. Sync with my development repo. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
  23. Adjust Imperative List/Map/Set Specification for more lenient next operation

    This allows implementations of this iterator specification to make use of
    temporary variables for obtaining the next element of the list/set/map.
    This is required by some and especially more general iterators. — n.muendler <n.muendler@tum.de> / hgweb
  24. discontinued obsolete "val extend = I" for data slots; — wenzelm / hgweb
  25. tuned; — wenzelm / hgweb
  26. merged — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
  27. metadata update for MFODL_Monitor_Optimized — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
  28. fixed a mistake in MFODL_Monitor_Optimized — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
  29. merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  30. adjusted Virtual-Substitution from 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  31. merge of AFP 2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  32. fixed duplicate "and" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  33. sitegen for Virtual_Substitution — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  34. new entry: Virtual Substitution — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  35. updated website/email address — Manuel Eberl <manuel@pruvisto.org> / hgweb
  36. modifications in Jinja and DOminance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
  37. modifications in Jinja and Dominance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
  38. modifications in Jinja and Dominance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
  39. merged — wenzelm / hgweb
  40. adapted to Term.dest_abs_global / Logic.dest_all_global (e.g. Isabelle/f07761ee5a7f); — wenzelm / hgweb
  41. more accurate treatment of context; — wenzelm / hgweb
  42. more accurate treatment of context; — wenzelm / hgweb
  43. more accurate treatment of context; — wenzelm / hgweb
  44. tuned -- proper names/scopes for contexts; — wenzelm / hgweb
  45. tuned proofs; — wenzelm / hgweb
  46. more accurate treatment of context; — wenzelm / hgweb
  47. more accurate treatment of context; — wenzelm / hgweb
  48. proper antiquotations; — wenzelm / hgweb
  49. tuned messages; — wenzelm / hgweb
  50. more maintainable Isabelle/ML: proper signatures, proper names/scopes for contexts;
    tuned whitespace; — wenzelm / hgweb
  51. dead code!? — wenzelm / hgweb
  52. clarified signature, following Isabelle/de4f151c2a34; — wenzelm / hgweb

#75 (Oct 24, 2021, 12:14:00 AM)

  1. added Mirabelle action presburger — desharna / hgweb
  2. added timing to Mirabelle action arith — desharna / hgweb
  3. added error message on invalid Mirabelle action — desharna / hgweb

#75 (Oct 24, 2021, 12:14:00 AM)

  1. CZH: large limits, generalizations, a variety of minor amendments — user9716869 <user9716869@gmail.com> / hgweb

#74 (Oct 17, 2021, 12:14:00 AM)

  1. A few new lemmas plus some refinements — paulson <lp15@cam.ac.uk> / hgweb
  2. merged — desharna / hgweb
  3. produced Mirabelle output directly in ML until Scala output gets fixed — desharna / hgweb
  4. clarified signature; — wenzelm / hgweb
  5. clarified signature; — wenzelm / hgweb
  6. clarified signature; — wenzelm / hgweb
  7. removed unused material (left-over from fd0c85d7da38); — wenzelm / hgweb
  8. support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a); — wenzelm / hgweb
  9. removed junk; — wenzelm / hgweb
  10. merged — nipkow / hgweb
  11. separated commands from annotations to be able to abstract about the latter only — nipkow / hgweb
  12. prefer standard Term.dest_abs, with minor deviation of generated names; — wenzelm / hgweb
  13. tuned comments; — wenzelm / hgweb
  14. more examples — nipkow / hgweb
  15. workaround for old macOS versions, after change of Let's Encrypt root certificate --- see also https://letsencrypt.org/docs/dst-root-ca-x3-expiration-september-2021 --- Java/Scala Isabelle_System.download() works, but curl doens't; — wenzelm / hgweb
  16. more complete simp rules — haftmann / hgweb
  17. more complete simp rules — haftmann / hgweb
  18. avoid overaggressive contraction of conversions — haftmann / hgweb
  19. normalizing NOT (numeral _) (again) — haftmann / hgweb

#74 (Oct 17, 2021, 12:14:00 AM)

  1. Simplified a definition — paulson <lp15@cam.ac.uk> / hgweb
  2. modify propa — nanjiang <nanjiang@whu.edu.cn> / hgweb
  3. bit singleton shifts recovered for the sake of backward compatibility — haftmann / hgweb
  4. updated to 7422950f3955 — nipkow / hgweb
  5. merge — Alexander Bentkamp <a.bentkamp@vu.nl> / hgweb
  6. EPO: simplify proof — Alexander Bentkamp <a.bentkamp@vu.nl> / hgweb
  7. primer — haftmann / hgweb
  8. more complete simp rules — haftmann / hgweb
  9. more complete simp rules (examples) — haftmann / hgweb
  10. avoid overaggressive contraction of conversions — haftmann / hgweb
  11. slightly more prominence for proof tools; more examples — haftmann / hgweb

#73 (Oct 10, 2021, 12:14:00 AM)

  1. tuned text; — wenzelm / hgweb
  2. recover NEWS from 78d1f73bbeaa; — wenzelm / hgweb
  3. save 90 MB by excluding rlwrap and thus perl; — wenzelm / hgweb
  4. save 45 MB by excluding rlwrap and thus perl; — wenzelm / hgweb
  5. NEWS; — wenzelm / hgweb
  6. clarified test of directories; — wenzelm / hgweb
  7. misc tuning for release; — wenzelm / hgweb
  8. merged — wenzelm / hgweb
  9. updated to kodkodi-1.5.7. with more robust/portable management of files and processes; — wenzelm / hgweb
  10. provide minisat-2.2.1 on all currently supported platforms, notably as external solver for Nitpick; — wenzelm / hgweb
  11. tuned message; — wenzelm / hgweb
  12. proper build on macOS; — wenzelm / hgweb
  13. build minisat, using recent fork from original sources; — wenzelm / hgweb
  14. proper platform_path for executables run from Java; — wenzelm / hgweb
  15. tuned message; — wenzelm / hgweb
  16. tuned; — wenzelm / hgweb
  17. tuned whitespace; — wenzelm / hgweb
  18. merged — desharna / hgweb
  19. added timeout to veriT — desharna / hgweb
  20. new notion of infinite sums in HOL-Analysis, ordering on complex numbers — eberlm <eberlm@in.tum.de> / hgweb
  21. NEWS and CONTRIBUTORS — desharna / hgweb
  22. merged — desharna / hgweb
  23. added offset to Mirabelle's tptp output names — desharna / hgweb
  24. tuned zipperposition config in sledgehammer — desharna / hgweb
  25. considered slices overhead in sledgehammer — desharna / hgweb
  26. tuned atp_prover sliding — desharna / hgweb
  27. tuned Zipperposition slides in sledgehammer — desharna / hgweb
  28. include arm64-linux; — wenzelm / hgweb
  29. updated to Vampire 4.6, as proposed by Martin Desharnais; — wenzelm / hgweb
  30. build from official downloads; — wenzelm / hgweb
  31. build just one vampire version; — wenzelm / hgweb
  32. clarified signature; — wenzelm / hgweb
  33. maintain previous theory identifier to support semantic caching, notably in Isabelle/Naproche; — wenzelm / hgweb
  34. more exports, notably for Isabelle/Naproche; — wenzelm / hgweb
  35. include arm64-linux; — wenzelm / hgweb
  36. prefer existing OCaml installation; — wenzelm / hgweb
  37. include arm64-linux; — wenzelm / hgweb
  38. no patchelf on macOS (undetected due to cached executables?); — wenzelm / hgweb
  39. provide opam-2.1.0 for experimentation; — wenzelm / hgweb
  40. rebuild cygwin-20211004.tar.gz; — wenzelm / hgweb
  41. include arm64-linux; — wenzelm / hgweb
  42. updated to cygwin-20211004: build again; — wenzelm / hgweb
  43. merged — wenzelm / hgweb
  44. removed pointless NEWS: both Docker/ubuntu and Cygwin provide perl by default; — wenzelm / hgweb
  45. actually use cygwin-20211002 (amending ff0ca375457c); — wenzelm / hgweb
  46. discontinued perl; — wenzelm / hgweb
  47. clarified signature; — wenzelm / hgweb
  48. proper term operation Term.dest_abs; — wenzelm / hgweb
  49. tuned; — wenzelm / hgweb
  50. tuned proofs;
    fewer warnings; — wenzelm / hgweb
  51. more standard binder syntax; — wenzelm / hgweb
  52. clarified 'let' syntax: avoid conflict with existing 'let' in FOL; — wenzelm / hgweb
  53. tuned; — wenzelm / hgweb
  54. tuned; — wenzelm / hgweb
  55. merged — paulson / hgweb
  56. removal of a redundant theorem (and white space) — paulson <lp15@cam.ac.uk> / hgweb
  57. new material from the Roth development, mostly about finite sets, disjoint famillies and partitions — paulson <lp15@cam.ac.uk> / hgweb
  58. clarified and updated for release; — wenzelm / hgweb
  59. formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc; — wenzelm / hgweb
  60. more NEWS and CONTRIBUTORS; — wenzelm / hgweb
  61. clarified comments; — wenzelm / hgweb
  62. support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing); — wenzelm / hgweb
  63. clarified dependencies; — wenzelm / hgweb
  64. updated for release; — wenzelm / hgweb
  65. Added tag Isabelle2021-1-RC0 for changeset fedc0b659881 — isatest / hgweb
  66. provide Isabelle/jEdit plugins as services, and thus allow user components do the same; — wenzelm / hgweb
  67. merged — wenzelm / hgweb
  68. updated for release; — wenzelm / hgweb
  69. misc tuning for release; — wenzelm / hgweb
  70. update dependency; — wenzelm / hgweb
  71. trim whitespace; — wenzelm / hgweb
  72. misc tuning for release; — wenzelm / hgweb
  73. misc tuning for release; — wenzelm / hgweb
  74. isabelle build_components -u; — wenzelm / hgweb
  75. updated to Haskell Stach lts-18.12 with GHC ghc-8.10.7; — wenzelm / hgweb
  76. updated to current Cygwin, near 3.2.0;
    discontinued perl; — wenzelm / hgweb
  77. updated to sumatra_pdf-3.3.3; — wenzelm / hgweb
  78. updated default version; — wenzelm / hgweb
  79. updated to xz-java-1.9; — wenzelm / hgweb
  80. updated to sqlite-jdbc-3.36.0.3; — wenzelm / hgweb
  81. updated to postgresql-42.2.24; — wenzelm / hgweb
  82. updated to jfreechart-1.5.3; — wenzelm / hgweb
  83. updated to flatlaf-1.6; — wenzelm / hgweb
  84. clarified signature; — wenzelm / hgweb
  85. clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax; — wenzelm / hgweb
  86. clarified sledgehammer_provers, following d8dc8fdc46fc; — wenzelm / hgweb
  87. proper term operation Term.dest_abs; — wenzelm / hgweb
  88. tuned, following Syntax_Trans.variant_abs; — wenzelm / hgweb
  89. proper patterns for (- numeral t), amending 03ff4d1e6784; — wenzelm / hgweb
  90. tuned; — wenzelm / hgweb
  91. merged — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
  92. update syntax for verit — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
  93. clarified antiquotations; — wenzelm / hgweb
  94. clarified antiquotations; — wenzelm / hgweb
  95. provide verit-2021.06-rmx; — wenzelm / hgweb

#73 (Oct 10, 2021, 12:14:00 AM)

  1. ETTS: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
  2. CTR and ETTS: integration with fd5f62176987 — user9716869 <user9716869@gmail.com> / hgweb
  3. adapted QHLProver to isabelle-dev/409ca22dee4c — Manuel Eberl <eberlm@in.tum.de> / hgweb
  4. adapted to isabelle-dev/409ca22dee4c — Manuel Eberl <eberlm@in.tum.de> / hgweb
  5. adapted to devel — nipkow / hgweb
  6. Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  7. Weighted_Path_Order: update to isabelle@ffb15f7f26d5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  8. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  9. add missing session dependency — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  10. new entry FOL_Axiomatic — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  11. regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  12. minor editorial changes for CZH entries — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  13. New entry Weighted_Path_Order — nipkow / hgweb
  14. fxed metadata (forgot .html) in link — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  15. metadata and sitegen for complex bounded operators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  16. new entry: Complex_Bounded_Operators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  17. restructure resultant algorithms, so that tuned code-equations are also availalbe for integral domains — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  18. removed obselete sorted_sorted_wrt, following Isabelle/06aeb9054c07; — wenzelm / hgweb
  19. clarified timeout;
    tuned whitespace; — wenzelm / hgweb
  20. hide_lams ~> opaque_lifting; — wenzelm / hgweb
  21. clarified antiquotations; — wenzelm / hgweb
  22. proper inst table; — wenzelm / hgweb
  23. clarified antiquotations; — wenzelm / hgweb
  24. clarified antiquotations; — wenzelm / hgweb
  25. proper inst table; — wenzelm / hgweb
  26. clarified antiquotations; — wenzelm / hgweb
  27. clarified antiquotations; — wenzelm / hgweb
  28. clarified antiquotations; — wenzelm / hgweb
  29. clarified antiquotations; — wenzelm / hgweb
  30. unused; — wenzelm / hgweb
  31. merged — wenzelm / hgweb
  32. clarified antiquotations; — wenzelm / hgweb
  33. proper match against const_name; — wenzelm / hgweb
  34. tuned; — wenzelm / hgweb
  35. tuned; — wenzelm / hgweb
  36. clarified antiquotations; — wenzelm / hgweb
  37. clarified antiquotations; — wenzelm / hgweb
  38. clarified antiquotations; — wenzelm / hgweb
  39. fix(ci): clarified addresses, set proper TLS version; — Fabian Huch <huch@in.tum.de> / hgweb
  40. feat(ci): remove hard-coded address; — Fabian Huch <huch@in.tum.de> / hgweb
  41. feat(SpecCheck/Show) tune pretty printing for environments — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  42. merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  43. eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  44. new entries by Mihails Milehins

    CZH_Elementary_Categories, CZH_Foundations,
    CZH_Universal_Constructions, Conditional_Simplification,
    Conditional_Transfer_Rule, Intro_Dest_Elim, and Types_To_Sets_Extension — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  45. New entry: Dominance_CHK — nipkow / hgweb
  46. Schutz_Spacetime website — paulson <lp15@cam.ac.uk> / hgweb
  47. new entry Schutz_Spacetime — paulson <lp15@cam.ac.uk> / hgweb
  48. metadata for Logging_Independent_Anonymity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  49. new entry Logging_Independent_Anonymity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb

#72 (Oct 3, 2021, 12:14:00 AM)

  1. clarified antiquotations; — wenzelm / hgweb
  2. merged — wenzelm / hgweb
  3. clarified antiquotations;
    some comments concerning odd "- numeral"; — wenzelm / hgweb
  4. clarified antiquotations; — wenzelm / hgweb
  5. clarified antiquotations; — wenzelm / hgweb
  6. merged — desharna / hgweb
  7. tuned TPTP parsing of THF function application — desharna / hgweb
  8. clarified examples; — wenzelm / hgweb
  9. repaired slip — haftmann / hgweb
  10. merged — desharna / hgweb
  11. updated to Zipperposition 2.1 — desharna / hgweb
  12. fixed veriT environment variable in sledgehammer's documentation — desharna / hgweb
  13. avoid overlapping PIDE markup (amending bb25ea271b15); — wenzelm / hgweb
  14. recover some Linux test, using virtual machine node (Ubuntu 20.04, 4 cores, 16 GB); — wenzelm / hgweb
  15. clarified antiquotations; — wenzelm / hgweb
  16. merged — wenzelm / hgweb
  17. clarified antiquotations; — wenzelm / hgweb
  18. clarified antiquotations; — wenzelm / hgweb
  19. clarified antiquotations; — wenzelm / hgweb
  20. clarified antiquotations; — wenzelm / hgweb
  21. clarified antiquotations; — wenzelm / hgweb
  22. clarified positions, notably for ML compiler errors; — wenzelm / hgweb
  23. clarified message; — wenzelm / hgweb
  24. proper default for Sledgehammer GUI panel; — wenzelm / hgweb
  25. tuned antiquotations; — wenzelm / hgweb
  26. more convenient ML arguments: avoid excessive nesting of cartouches; — wenzelm / hgweb
  27. outer syntax: support for control-cartouche tokens; — wenzelm / hgweb
  28. merged — nipkow / hgweb
  29. An example — nipkow / hgweb
  30. prefer veriT over Z3 in sledgehammer — desharna / hgweb
  31. added Zipperposition to sledgehammer's default provers — desharna / hgweb
  32. provide zipperposition-2.1 (still unused); — wenzelm / hgweb
  33. tuned docs — blanchet / hgweb
  34. merged — wenzelm / hgweb
  35. improper proof command 'guess' moved to separate theory "Pure-ex.Guess"; — wenzelm / hgweb
  36. NOT is part of syntax bundle also — haftmann / hgweb

#72 (Oct 3, 2021, 12:14:00 AM)

  1. repaired slip — haftmann / hgweb
  2. feat(SpecCheck) folder renaming, types for tests — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  3. tuned — nipkow / hgweb
  4. mproper proof command 'guess' moved to separate theory "Pure-ex.Guess", according to Isabelle/b49bd5d9041f; — wenzelm / hgweb

#71 (Sep 26, 2021, 12:14:00 AM)

  1. merged — wenzelm / hgweb
  2. tuned proofs --- avoid 'guess'; — wenzelm / hgweb
  3. apply declarations from interpretations in eigen context also — haftmann / hgweb
  4. grant access to sun.tools.jconsole, as required for Java 17; — wenzelm / hgweb
  5. update to e-2.6, following Martin Desharnais; — wenzelm / hgweb
  6. updated to Metis 2.4 (release 20200713) — desharna / hgweb
  7. avoid problems with launch4j and jdk-17; — wenzelm / hgweb
  8. update to jdk-17+35 (LTS); — wenzelm / hgweb
  9. tuned message; — wenzelm / hgweb
  10. unused since 398b7bb9ebdd; — wenzelm / hgweb
  11. merged — desharna / hgweb
  12. removed checks for non-commercial usage of Vampire as it is now under BSD licence — desharna / hgweb
  13. enabled FOOL for Vampire in Sledgehammer — desharna / hgweb
  14. used Vampire 4.5.1 in Sledgehammer — desharna / hgweb
  15. proper NEWS; — wenzelm / hgweb
  16. tuned NEWS; — wenzelm / hgweb
  17. clarified antiquotations; — wenzelm / hgweb
  18. clarified antiquotations; — wenzelm / hgweb
  19. clarified antiquotations; — wenzelm / hgweb
  20. clarified partial application: immediate check of object-logic, and avoidance of context within closure; — wenzelm / hgweb
  21. merged — wenzelm / hgweb
  22. clarified antiquotations; — wenzelm / hgweb
  23. ML antiquotations for object-logic judgment; — wenzelm / hgweb
  24. proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep; — wenzelm / hgweb
  25. clarified modules; — wenzelm / hgweb
  26. clarified modules; — wenzelm / hgweb
  27. more uniform syntax; — wenzelm / hgweb
  28. permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone; — wenzelm / hgweb
  29. NEWS; — wenzelm / hgweb
  30. bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; — wenzelm / hgweb
  31. localized command 'syntax' and 'no_syntax'; — wenzelm / hgweb
  32. tuned; — wenzelm / hgweb
  33. clarified signature; — wenzelm / hgweb
  34. clarified signature; — wenzelm / hgweb
  35. merged — desharna / hgweb
  36. proper constants in TPTP $let binding — desharna / hgweb
  37. more operations from Isabelle/ML; — wenzelm / hgweb
  38. merged — wenzelm / hgweb
  39. tuned proofs --- eliminated 'guess'; — wenzelm / hgweb
  40. tuned proofs;
    tuned whitespace; — wenzelm / hgweb
  41. clarified antiquotations; — wenzelm / hgweb
  42. proper firstorderization in Sledgehammer — desharna / hgweb
  43. clarified signature;
    clarified antiquotations; — wenzelm / hgweb
  44. clarified antiquotations; — wenzelm / hgweb
  45. clarified signature -- prefer antiquotations (with subtle change of exception content); — wenzelm / hgweb
  46. more control symbols; — wenzelm / hgweb
  47. support ML antiquotations with fn abstraction; — wenzelm / hgweb
  48. unused; — wenzelm / hgweb

#71 (Sep 26, 2021, 12:14:00 AM)

  1. ported Design-Theory from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  2. ported Three-Circles from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  3. move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  4. ported Cubic_Quartic_Equations from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  5. merge of AFP 2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  6. Cubic_Quartic_Equations sitegen — paulson <lp15@cam.ac.uk> / hgweb
  7. new entry Cubic_Quartic_Equations — paulson <lp15@cam.ac.uk> / hgweb
  8. sitegen for combinatorial design theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  9. new entry: Combinatorial Design Theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  10. sitegen for Three Circles — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  11. new entry: Three Circles — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  12. clarified modules, according to Isabelle/534b231ce041; — wenzelm / hgweb
  13. bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax, according to Isabelle/ead56ad40e15;
    subtle change of inf (infixl "\<sqinter>" 70) vs. (infixl "\<sqinter>" 65); — wenzelm / hgweb
  14. clarified signature, according to Isabelle/d882abae3379; — wenzelm / hgweb

#70 (Sep 19, 2021, 12:14:00 AM)

  1. clarified operations: follow Isabelle/ML more closely; — wenzelm / hgweb
  2. provide current vampire-4.5.1: presently unused in Sledgehammer, but relevant for Isabelle/Naproche; — wenzelm / hgweb
  3. obsolete; — wenzelm / hgweb
  4. tuned; — wenzelm / hgweb
  5. clarified name and options for old vampire-4.2.2; — wenzelm / hgweb
  6. clarified signature; — wenzelm / hgweb
  7. explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell) — haftmann / hgweb
  8. more latex macros; — wenzelm / hgweb
  9. tuned; — wenzelm / hgweb
  10. clarified signature; — wenzelm / hgweb
  11. more antiquotations; — wenzelm / hgweb
  12. more antiquotations; — wenzelm / hgweb
  13. more antiquotations; — wenzelm / hgweb
  14. more antiquotations;
    more formal use of consts; — wenzelm / hgweb
  15. more antiquotations;
    more formal use of consts; — wenzelm / hgweb
  16. clarified antiquotations; — wenzelm / hgweb
  17. more antiquotations; — wenzelm / hgweb
  18. more antiquotations; — wenzelm / hgweb
  19. more antiquotations; — wenzelm / hgweb
  20. clarified antiquotation; — wenzelm / hgweb
  21. more antiquotations; — wenzelm / hgweb
  22. more antiquotations; — wenzelm / hgweb
  23. more antiquotations; — wenzelm / hgweb
  24. tuned; — wenzelm / hgweb
  25. ML antiquotations for type constructors and term constants; — wenzelm / hgweb
  26. more antiquotations; — wenzelm / hgweb

#70 (Sep 19, 2021, 12:14:00 AM)

  1. explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell) — haftmann / hgweb
  2. tuned signature, according to Isabelle/28a582aa25dd; — wenzelm / hgweb

#69 (Sep 12, 2021, 12:14:00 AM)

  1. tuned; — wenzelm / hgweb
  2. NEWS; — wenzelm / hgweb
  3. miscellaneous examples and experiments for Isabelle/Pure; — wenzelm / hgweb
  4. tuned comments; — wenzelm / hgweb
  5. unused; — wenzelm / hgweb
  6. clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference); — wenzelm / hgweb
  7. NEWS; — wenzelm / hgweb
  8. clarified signature: more scalable operations; — wenzelm / hgweb
  9. more scalable operations; — wenzelm / hgweb
  10. more scalable operations; — wenzelm / hgweb
  11. clarified order of extra type variables, following names more often than occurrences; — wenzelm / hgweb
  12. clarified signature;
    tuned; — wenzelm / hgweb
  13. tuned; — wenzelm / hgweb
  14. more scalable operations; — wenzelm / hgweb
  15. omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused; — wenzelm / hgweb
  16. clarified signature; — wenzelm / hgweb
  17. more robust: client could have terminated already; — wenzelm / hgweb
  18. clarified signature; — wenzelm / hgweb
  19. clarified signature; — wenzelm / hgweb
  20. clarified modules; — wenzelm / hgweb
  21. clarified set of items with order of addition; — wenzelm / hgweb
  22. tuned message; — wenzelm / hgweb
  23. tuned whitespace; — wenzelm / hgweb
  24. clarified signature;
    clarified modules; — wenzelm / hgweb
  25. tuned; — wenzelm / hgweb
  26. simplified: uniqueness check happens in export_consumer; — wenzelm / hgweb
  27. more markup, e.g. to locate defining theory node in formal document output; — wenzelm / hgweb
  28. tuned signature; — wenzelm / hgweb
  29. export other entities, e.g. relevant for formal document output;
    clarified markup kind (PIDE) vs. export kind (e.g. MMT); — wenzelm / hgweb
  30. pointer_eq_ord: minor performance tuning; — wenzelm / hgweb
  31. more robust: progress.stopped means that build has failed; — wenzelm / hgweb
  32. more reactive interrupt; — wenzelm / hgweb
  33. more reactive interrupt; — wenzelm / hgweb
  34. more robust: retain length of results; — wenzelm / hgweb
  35. more reactive interrupt; — wenzelm / hgweb
  36. tuned signature; — wenzelm / hgweb
  37. tuned signature; — wenzelm / hgweb
  38. tuned signature; — wenzelm / hgweb
  39. tuned; — wenzelm / hgweb
  40. merged — wenzelm / hgweb
  41. clarified modules; — wenzelm / hgweb
  42. more scalable operations; — wenzelm / hgweb
  43. more scalable operations; — wenzelm / hgweb
  44. tuned; — wenzelm / hgweb
  45. clarified modules; — wenzelm / hgweb
  46. clarified signature;
    minor performance tuning; — wenzelm / hgweb
  47. more scalable operations; — wenzelm / hgweb
  48. unused; — wenzelm / hgweb
  49. more efficient operations: traverse hyps only when required; — wenzelm / hgweb
  50. more robust signature: result has no particular order; — wenzelm / hgweb
  51. more scalable operations; — wenzelm / hgweb
  52. unused; — wenzelm / hgweb
  53. more scalable operations; — wenzelm / hgweb
  54. clarified; — wenzelm / hgweb
  55. tuned signature; — wenzelm / hgweb
  56. clarified signature; — wenzelm / hgweb
  57. more scalable operations; — wenzelm / hgweb
  58. clarified signature; — wenzelm / hgweb
  59. tuned signature; — wenzelm / hgweb
  60. more scalable operations; — wenzelm / hgweb
  61. more scalable operations; — wenzelm / hgweb
  62. more scalable operations;
    tuned; — wenzelm / hgweb
  63. more scalable operations; — wenzelm / hgweb
  64. white space — paulson <lp15@cam.ac.uk> / hgweb
  65. merged — paulson / hgweb
  66. some fixes connected with card_Diff_singleton — paulson <lp15@cam.ac.uk> / hgweb
  67. strengthened a few lemmas about finite sets and added a code equation for complex_of_real — paulson <lp15@cam.ac.uk> / hgweb
  68. tuned; — wenzelm / hgweb
  69. proper inst table; — wenzelm / hgweb
  70. more scalable data structure (but: rarely used many arguments); — wenzelm / hgweb
  71. minor performance tuning: fewer allocations;
    clarified theory context; — wenzelm / hgweb

#69 (Sep 12, 2021, 12:14:00 AM)

  1. eliminated Specification.definition', following Isabelle/6876e3d5e362; — wenzelm / hgweb
  2. clarified signature: more scalable operations, according to Isabelle/c2ee8d993d6a; — wenzelm / hgweb
  3. clarified signature, according to Isabelle/612b7e0d6721; — wenzelm / hgweb
  4. tuned signature, according to Isabelle/839a6e284545; — wenzelm / hgweb
  5. merged — sterraf / hgweb
  6. Backed out changeset ef19e4e58b8c
    restoring old argument order on synthesized formulas — sterraf / hgweb
  7. avoid hardwired document; — wenzelm / hgweb
  8. merged — wenzelm / hgweb
  9. tuned signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
  10. clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
  11. clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
  12. clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
  13. simplified, using Isabelle/ML operations; — wenzelm / hgweb
  14. adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for vars; — wenzelm / hgweb
  15. tuned whitespace; — wenzelm / hgweb
  16. more scalable operations; — wenzelm / hgweb
  17. merged — sterraf / hgweb
  18. synthesized formulas have their variables permuted — sterraf / hgweb
  19. merged — paulson / hgweb
  20. fixes for cardinality lemmas — paulson <lp15@cam.ac.uk> / hgweb
  21. proper inst table; — wenzelm / hgweb

#68 (Sep 5, 2021, 12:14:00 AM)

  1. tuned; — wenzelm / hgweb
  2. more Isabelle/Haskell operations; — wenzelm / hgweb
  3. more Isabelle/Haskell operations;
    tuned; — wenzelm / hgweb
  4. avoid change of existing file, notably rebuild via ghc_stack; — wenzelm / hgweb
  5. tuned signature; — wenzelm / hgweb
  6. more Isabelle/Haskell operations; — wenzelm / hgweb
  7. clarified process description; — wenzelm / hgweb
  8. more Isabelle/Haskell operations; — wenzelm / hgweb
  9. clarified signature; — wenzelm / hgweb

#67 (Aug 29, 2021, 12:14:00 AM)

  1. more Isabelle/Haskell; — wenzelm / hgweb
  2. made sure lambda-lifting works well with native let binders in Sledgehammer — blanchet / hgweb
  3. handle Zipperposition's ResourceOut gracefully — blanchet / hgweb
  4. disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax — blanchet / hgweb
  5. proper test for type constructor; — wenzelm / hgweb
  6. more Isabelle/Haskell operations; — wenzelm / hgweb
  7. more Isabelle/Haskell operations; — wenzelm / hgweb
  8. merged — wenzelm / hgweb
  9. tuned; — wenzelm / hgweb
  10. more scalable data structure (but: rarely used with > 5 arguments); — wenzelm / hgweb
  11. Backed out changeset d4af818e0880 — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  12. merged — wenzelm / hgweb
  13. more Isabelle/Haskell operations; — wenzelm / hgweb
  14. more Isabelle/Haskell operations; — wenzelm / hgweb
  15. tuned; — wenzelm / hgweb
  16. more Isabelle/Haskell operations; — wenzelm / hgweb
  17. reflect moved theories — nipkow / hgweb
  18. unhide canonical function def examples — nipkow / hgweb
  19. merged — nipkow / hgweb
  20. merged — nipkow / hgweb
  21. Backed out changeset fe8d0f4da0e6 — nipkow / hgweb
  22. more Isabelle/Haskell operations; — wenzelm / hgweb
  23. more Isabelle/Haskell operations; — wenzelm / hgweb
  24. more Isabelle/Haskell operations; — wenzelm / hgweb
  25. more Isabelle/Haskell operations; — wenzelm / hgweb
  26. clarified signature; — wenzelm / hgweb
  27. clarified signature; — wenzelm / hgweb
  28. minor performance tuning; — wenzelm / hgweb
  29. tuned; — wenzelm / hgweb
  30. tuned; — wenzelm / hgweb
  31. tuned signature; — wenzelm / hgweb
  32. tuned comments; — wenzelm / hgweb
  33. treat Symbol.eof as in ML (but: presently unused); — wenzelm / hgweb
  34. tuned; — wenzelm / hgweb
  35. minor performance tuning; — wenzelm / hgweb
  36. clarified signature; — wenzelm / hgweb
  37. proper Isabelle symbol positions; — wenzelm / hgweb
  38. more Haskell operations; — wenzelm / hgweb
  39. clarified signature; — wenzelm / hgweb
  40. tuned; — wenzelm / hgweb
  41. tuned; — wenzelm / hgweb
  42. tuned signature: prefer existing Haskell operations; — wenzelm / hgweb
  43. more Haskell operations; — wenzelm / hgweb
  44. tuned signature; — wenzelm / hgweb
  45. tuned comments; — wenzelm / hgweb
  46. tuned; — wenzelm / hgweb
  47. consolidation of rules for bit operations — haftmann / hgweb

#67 (Aug 29, 2021, 12:14:00 AM)

  1. Graphic rendering of Relational_Method PDF files refined. — Pasquale Noce <pasquale.noce@hidglobal.com> / hgweb
  2. Entry Relational_Method updated. — Pasquale Noce <pasquale.noce@hidglobal.com> / hgweb
  3. more realistic timeout; — wenzelm / hgweb
  4. clarified signature; — wenzelm / hgweb
  5. follow Isabelle/53e28c438f96; — wenzelm / hgweb
  6. clarified signature, following Isabelle/a3b0fc510705; — wenzelm / hgweb
  7. merged — nipkow / hgweb
  8. tuned — nipkow / hgweb
  9. consolidation of rules for bit operations — haftmann / hgweb

#66 (Aug 22, 2021, 12:14:00 AM)

  1. fixed $ite syntax in TPTP TFX generation — desharna / hgweb
  2. more Haskell operations; — wenzelm / hgweb
  3. merged — wenzelm / hgweb
  4. revert 0faa68dedce5: very slow; — wenzelm / hgweb
  5. tuned; — wenzelm / hgweb
  6. add/rename some theorems about Map(pings) — Lukas Stevens <mail@lukas-stevens.de> / hgweb
  7. support configuration options "show_results"; — wenzelm / hgweb
  8. consolidate_body more thoroughly, e.g. for reduced ML_Heap.obj_size; — wenzelm / hgweb
  9. merged — desharna / hgweb
  10. fixed $ite syntax in TPTP THX generation — desharna / hgweb
  11. tuned signature; — wenzelm / hgweb
  12. more scalable data structures; — wenzelm / hgweb
  13. more scalable data structures; — wenzelm / hgweb
  14. more scalable data structures;
    tuned; — wenzelm / hgweb
  15. proper position information for Context.theory_data_size; — wenzelm / hgweb

#66 (Aug 22, 2021, 12:14:00 AM)

  1. tuned name — nipkow / hgweb
  2. Fix typo — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
  3. Tune references

    ... using new name of BD_Security_Compositional — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
  4. Remove redundant license — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
  5. more realistic timeout: approx. 5min CPU time; — wenzelm / hgweb
  6. cleaning up — nipkow / hgweb
  7. New entry CoSMeDis — nipkow / hgweb
  8. New entry CoSMed — nipkow / hgweb
  9. New entry: BD_Security_Compositional — nipkow / hgweb
  10. New entry: CoCon — nipkow / hgweb
  11. updated to devel — nipkow / hgweb
  12. merge from AFP 2021 — nipkow / hgweb
  13. New entry Fresh_Identifiers — nipkow / hgweb
  14. New entry: Relational_Forests — nipkow / hgweb
  15. cleaning up — nipkow / hgweb
  16. merged — nipkow / hgweb
  17. cleaning up — nipkow / hgweb
  18. Update Bounded_Deducibility_Security

    - Generalise BD Security from I/O automata to nondeterministic transition
      systems, with the former retained as an instance of the latter (renaming
      locale BD_Security to BD_Security_IO)
    - Generalise unwinding conditions to allow making more than one transition at a
      time when constructing alternative traces, giving more flexibility for
      unwinding strategies
    - Add various helper lemmas and definitions
    - Add results about the expressivity of declassification triggers vs. bounds,
      due to Thomas Bauereiss (added as author) — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
  19. tuned signature, following Isabelle/069f6b2c5a07; — wenzelm / hgweb

#65 (Aug 15, 2021, 12:14:00 AM)

  1. provide bash_process server for Isabelle/ML and other external programs;
    clarified signature for Bash.params; — wenzelm / hgweb
  2. clarified signature; — wenzelm / hgweb
  3. clarified signature; — wenzelm / hgweb
  4. proper prover_options for batch-build; — wenzelm / hgweb
  5. clarified signature;
    clarified errors; — wenzelm / hgweb
  6. clarified signature: more options for bash_process; — wenzelm / hgweb
  7. tuned signature; — wenzelm / hgweb
  8. clarified signature; — wenzelm / hgweb
  9. clarified signature; — wenzelm / hgweb
  10. follow phabricator 2021 Week 26;
    follow arcanist 2021 Week 23; — wenzelm / hgweb
  11. tuned signature; — wenzelm / hgweb
  12. tuned; — wenzelm / hgweb
  13. clarified signature; — wenzelm / hgweb
  14. clarified signature; — wenzelm / hgweb
  15. unused; — wenzelm / hgweb
  16. clarified signature; — wenzelm / hgweb
  17. merged — wenzelm / hgweb
  18. clarified modules; — wenzelm / hgweb
  19. type classes for XML data representation; — wenzelm / hgweb
  20. tuned signature; — wenzelm / hgweb
  21. clarified types: prefer Isabelle byte strings; — wenzelm / hgweb
  22. merged — desharna / hgweb
  23. added option labels to Mirabelle actions — desharna / hgweb
  24. more operations: dest binders; — wenzelm / hgweb
  25. clarified abstract and concrete boolean algebras — haftmann / hgweb
  26. antiquotation for bundles — haftmann / hgweb
  27. prefer persistent hash code for cachable items (see also 72b13af7f266); — wenzelm / hgweb
  28. merged — wenzelm / hgweb
  29. more operations: record overall exported entities; — wenzelm / hgweb
  30. merged — desharna / hgweb
  31. added dummy_fof prover to Sledgehammer — desharna / hgweb
  32. fixed malconfigured option output_dir in mirabelle — desharna / hgweb
  33. merged — wenzelm / hgweb
  34. clarified export of formal entities: name space info is always present, but content depends on option "export_theory"; — wenzelm / hgweb
  35. proper name space "kind": this is a formal name, not comment; — wenzelm / hgweb
  36. more uniform signatures in ML and Scala; — wenzelm / hgweb
  37. merged — desharna / hgweb
  38. fixed typo — desharna / hgweb
  39. added dummy_thf prover to Sledgehammer — desharna / hgweb
  40. simplified hierarchy of type classes for bit operations — haftmann / hgweb
  41. obsolete — haftmann / hgweb
  42. more operations, notably free and bound variables as in Isabelle/Pure; — wenzelm / hgweb
  43. more operations on types and terms;
    abstract syntax operations for Pure and HOL; — wenzelm / hgweb
  44. clarified jEdit java sources; — wenzelm / hgweb
  45. clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for unknown reasons; — wenzelm / hgweb
  46. removed junk; — wenzelm / hgweb
  47. moved theory Bit_Operations into Main corpus — haftmann / hgweb
  48. more operations; — wenzelm / hgweb
  49. clarified signature; — wenzelm / hgweb
  50. clarified signature; — wenzelm / hgweb
  51. organize syntax for word operations in bundles — haftmann / hgweb
  52. support for Lazy.Text; — wenzelm / hgweb
  53. prefer compact Isabelle.Bytes; — wenzelm / hgweb
  54. clarified signature; — wenzelm / hgweb
  55. clarified signature --- more operations; — wenzelm / hgweb
  56. tuned; — wenzelm / hgweb
  57. clarified order of modules; — wenzelm / hgweb
  58. more operations; — wenzelm / hgweb
  59. tuned; — wenzelm / hgweb

#65 (Aug 15, 2021, 12:14:00 AM)

  1. metadata update for MFMC_Countable — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  2. derive rel_pmf characterization from bounded and unbounded MFMC theorem — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  3. merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  4. drop boundedness requirement for the sink — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  5. avoid global tmp file: pointless due to implicit theory export; — wenzelm / hgweb
  6. repaired syntax — haftmann / hgweb
  7. tuned signature, following Isabelle/d030b988d470; — wenzelm / hgweb
  8. generalized gt_rat_sign_change to square-free polynomials — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  9. minor updates to bibliography — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  10. clarified signature; — wenzelm / hgweb
  11. clarified abstract and concrete boolean algebras — haftmann / hgweb
  12. antiquotation for bundles — haftmann / hgweb
  13. simplified hierarchy of type classes for bit operations — haftmann / hgweb
  14. restored executable conversions — haftmann / hgweb
  15. dropped junk — haftmann / hgweb
  16. moved theory Bit_Operations into Main corpus — haftmann / hgweb
  17. organize syntax for word operations in bundles — haftmann / hgweb
  18. more systematic approach for instantiation — haftmann / hgweb
  19. avoid seemingly unused transfer rules — haftmann / hgweb

#63 (Aug 1, 2021, 12:14:00 AM)

  1. clarified signature; — wenzelm / hgweb
  2. tuned signature; — wenzelm / hgweb
  3. clarified signature; — wenzelm / hgweb
  4. merged — wenzelm / hgweb
  5. prefer Isabelle.Bytes, based on ShortByteString; — wenzelm / hgweb
  6. tuned; — wenzelm / hgweb
  7. tuned signature; — wenzelm / hgweb
  8. tuned signature: more generic operations; — wenzelm / hgweb
  9. prefer UTF8 implementation from Data.Text.Encoding (foreign C);
    clarified signatures and modules; — wenzelm / hgweb
  10. documented Mirabelle_Sledgehammer's new keep semantics — desharna / hgweb
  11. changed Mirabelle_Sledgehammer keep option from path to boolean — desharna / hgweb
  12. added automatic uniform stride option to Mirabelle — desharna / hgweb
  13. fixed HOL-ex following a5bab59d580b — desharna / hgweb
  14. added support for TFX $let to Sledgehammer's TPTP output — desharna / hgweb
  15. merged — desharna / hgweb
  16. fixed TFX generation when universal quantifier is used as term — desharna / hgweb
  17. merged — wenzelm / hgweb
  18. various improvements of "isabelle scala_project"; — wenzelm / hgweb
  19. support for native symlinks on Windows; — wenzelm / hgweb
  20. tuned Mirabelle's theory selection — desharna / hgweb
  21. clarified signature; — wenzelm / hgweb
  22. clarified signature; — wenzelm / hgweb
  23. updated for Isabelle2021 release; — wenzelm / hgweb
  24. back to stackage lts-17.10, to make this work on vmnipkow9 (Windows Server 2012 R2); — wenzelm / hgweb
  25. update to Haskell stack-2.7.3 and stackage lts-17.15; — wenzelm / hgweb
  26. clarified version: Apple now counts like 11, 12, ...; — wenzelm / hgweb

#63 (Aug 1, 2021, 12:14:00 AM)

  1. cleaner presentation of analysis theorems in preliminaries — yonoteam / hgweb
  2. Update to new Epistemic_Logic.thy — Asta Halkjær From <andro.from@gmail.com> / hgweb
  3. Avoid typedefs — Asta Halkjær From <andro.from@gmail.com> / hgweb
  4. Clean: set AFP standard document options — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  5. Clean: re-add to chapter AFP — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  6. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  7. Finitely_Generated_Abelian_Groups website — paulson <lp15@cam.ac.uk> / hgweb
  8. new entry Finitely_Generated_Abelian_Groups — paulson <lp15@cam.ac.uk> / hgweb
  9. Added Finitely_Generated_Abelian_Groups to metadata — Manuel Eberl <eberlm@in.tum.de> / hgweb

#62 (Jul 25, 2021, 12:14:00 AM)

  1. clarified signature; — wenzelm / hgweb
  2. clarified compiler output: allow multithreaded execution; — wenzelm / hgweb
  3. clarified signature: more operations; — wenzelm / hgweb
  4. clarified props: more permissive; — wenzelm / hgweb
  5. more robust; — wenzelm / hgweb
  6. clarified properties: "module" and "no_build";
    clarified signature; — wenzelm / hgweb
  7. clarified signature; — wenzelm / hgweb
  8. clarified signature; — wenzelm / hgweb
  9. tuned comments; — wenzelm / hgweb
  10. tuned document; — wenzelm / hgweb
  11. clarified names (again), e.g. relevant for "Plugin Options"; — wenzelm / hgweb
  12. added simp_options to meson — desharna / hgweb
  13. tuning — blanchet / hgweb
  14. parse TPTP operator @ also when not parenthesized — blanchet / hgweb
  15. removed setup for outdated CVC3 from Isabelle — blanchet / hgweb
  16. tuned E's lambda encoding — blanchet / hgweb
  17. use Vampire's clausifier with iProver, now that E's is no longer supported — blanchet / hgweb
  18. updated Sledgehammer docs -- removed most version numbers since these are tedious to maintain — blanchet / hgweb
  19. compile — blanchet / hgweb
  20. tuned; — wenzelm / hgweb
  21. NEWS; — wenzelm / hgweb
  22. updated documentation on Isabelle/Scala; — wenzelm / hgweb
  23. discontinued obsolete Apple (deprecated); — wenzelm / hgweb
  24. clarified component setup: exclude jar from active component, but use sources from template within ISABELLE_HOME (relevant for "isabelle scala_project -L"); — wenzelm / hgweb
  25. more robust "isabelle build_scala" as separate tool; — wenzelm / hgweb
  26. tuned --- based on hints by IntelliJ IDEA; — wenzelm / hgweb
  27. more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in AFP/1001c0dfced0); — wenzelm / hgweb
  28. more portable across history; — wenzelm / hgweb
  29. proper isabelle.setup.Setup build; — wenzelm / hgweb
  30. rebuild component; — wenzelm / hgweb
  31. more complete scala_project, including Isabelle/jEdit plugins; — wenzelm / hgweb
  32. clarified directories; — wenzelm / hgweb
  33. more accurate scala_project, based on build.props of components; — wenzelm / hgweb
  34. clarified build_props: empty module means no build;
    clarified signature;
    clarified errors; — wenzelm / hgweb
  35. tuned; — wenzelm / hgweb
  36. CONTRIBUTORS — haftmann / hgweb
  37. merged — wenzelm / hgweb
  38. more robust; — wenzelm / hgweb
  39. rebuild component; — wenzelm / hgweb
  40. more robust: for the sake of Isabelle.app on macOS; — wenzelm / hgweb
  41. more robust; — wenzelm / hgweb
  42. more robust; — wenzelm / hgweb
  43. more robust; — wenzelm / hgweb
  44. rebuild component; — wenzelm / hgweb
  45. more informative errors: capture low-level compiler output; — wenzelm / hgweb
  46. more direct isabelle_scala_build: always enabled, no "Admin" requirement; — wenzelm / hgweb
  47. tuned --- fewer warnings; — wenzelm / hgweb
  48. clarified names; — wenzelm / hgweb
  49. tuned --- fewer warnings; — wenzelm / hgweb
  50. clarified directory; — wenzelm / hgweb
  51. clarified names; — wenzelm / hgweb
  52. clarified component setup for old graph browser; — wenzelm / hgweb
  53. redundant: *.class and *.jar are already ignored; — wenzelm / hgweb
  54. proper cat_lines: avoid last "\n"; — wenzelm / hgweb
  55. merged — paulson / hgweb
  56. A few new lemmas and simplifications — paulson <lp15@cam.ac.uk> / hgweb
  57. removed support for experimental Pirate prover — blanchet / hgweb

#62 (Jul 25, 2021, 12:14:00 AM)

  1. Sync with my development repo.  Add new material: "concrete bicategories" and
    "bicategory of categories".  Change sublocale declarations related to
    functor/natural transformation/natural isomorphism to avoid issues with
    global interpretations reported by Filip Smola, 2/2/2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb

#61 (Jul 18, 2021, 12:14:00 AM)

  1. get rid of remote_vampire since it's hard, if possible at all, to follow Vampire's online options — blanchet / hgweb
  2. merged — wenzelm / hgweb
  3. NEWS; — wenzelm / hgweb
  4. proper example; — wenzelm / hgweb
  5. more tests; — wenzelm / hgweb
  6. more robust: component might be absent; — wenzelm / hgweb
  7. clarified global state: allow to deactivate main plugin; — wenzelm / hgweb
  8. more robust (again): allow to deactivate main plugin; — wenzelm / hgweb
  9. tuned signature; — wenzelm / hgweb
  10. more complete dockables; — wenzelm / hgweb
  11. more robust (see 4d91b6d5d49c); — wenzelm / hgweb
  12. clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin; — wenzelm / hgweb
  13. more robust; — wenzelm / hgweb
  14. tuned; — wenzelm / hgweb
  15. avoid non-standard encoding; — wenzelm / hgweb
  16. proper cross-platform build: jdk component is required for ISABELLE_SETUP_CLASSPATH in other_isabelle; — wenzelm / hgweb
  17. more robust classpath: skip empty entries; — wenzelm / hgweb
  18. more robust: avoid duplicate classpath entries; — wenzelm / hgweb
  19. build.props for isabelle.jar, including isabelle.jedit;
    build minimal Isabelle/jEdit plugins on the spot;
    regular "jedit" component: discontinued special "jedit_build";
    Isabelle/Scala services via jars, instead of settings; — wenzelm / hgweb
  20. more robust; — wenzelm / hgweb
  21. more portable: avoid Windows CRLF in classpath output; — wenzelm / hgweb
  22. proper lines (amending 59b6f0462086); — wenzelm / hgweb
  23. more systematic treatment of encodings; — wenzelm / hgweb
  24. tuned; — wenzelm / hgweb
  25. extended the 'corec' format slightly — blanchet / hgweb
  26. prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent — blanchet / hgweb
  27. tuning — blanchet / hgweb
  28. rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option — blanchet / hgweb
  29. correctly translate constructor argument in 'primrec' — blanchet / hgweb
  30. simplified a few proofs — paulson <lp15@cam.ac.uk> / hgweb
  31. revisited ac28714b7478: more faithful preplaying with chained facts — blanchet / hgweb
  32. wait for E 2.7 before using 'ite' in HO mode — blanchet / hgweb
  33. added alternative E binary name — blanchet / hgweb
  34. parse logical operators in the right order w.r.t. backtracking — blanchet / hgweb
  35. improved warning — blanchet / hgweb
  36. adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing) — blanchet / hgweb
  37. operations for symbolic computation of bit operations — haftmann / hgweb
  38. proper local context — haftmann / hgweb
  39. shasum for project meta-info; — wenzelm / hgweb
  40. even more strict shasum (amending c9771e1b3223); — wenzelm / hgweb
  41. clarified Isabelle meta-info within jar; — wenzelm / hgweb
  42. strict shasum: this is used on input files; — wenzelm / hgweb
  43. clarified modules;
    clarified messages;
    clarified return code; — wenzelm / hgweb
  44. support for command-line operations; — wenzelm / hgweb
  45. operations for all components; — wenzelm / hgweb
  46. clarified signature; — wenzelm / hgweb
  47. merged — wenzelm / hgweb
  48. rebuild component; — wenzelm / hgweb
  49. expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER; — wenzelm / hgweb
  50. support expand_platform_path, which is reminiscent of isabelle.Path.expand; — wenzelm / hgweb
  51. skip scalac for Java build; — wenzelm / hgweb
  52. support mixed Scala/Java build;
    clarified scalac/javac options; — wenzelm / hgweb
  53. clarified javac options; — wenzelm / hgweb
  54. clarified syntax: similar to URL; — wenzelm / hgweb
  55. clarified signature; — wenzelm / hgweb
  56. more robust; — wenzelm / hgweb
  57. more robust; — wenzelm / hgweb
  58. more compiler_deps via "requirements", notably jar list from settings;
    proper Files.createDirectories; — wenzelm / hgweb
  59. clarified component settings; — wenzelm / hgweb
  60. clarified shasum: sources / resources within jar; — wenzelm / hgweb
  61. tuned signature; — wenzelm / hgweb
  62. clarified modules; — wenzelm / hgweb
  63. merged — desharna / hgweb
  64. fixed HOL-TPTP following f58108b7a60c — desharna / hgweb
  65. documented Sledgehammer option "induction_rules" — desharna / hgweb
  66. refactored Sledgehammer option "induction_rules" — desharna / hgweb
  67. promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules" — desharna / hgweb
  68. jenkins: add pre/post-hook results for benchmark — Fabian Huch <huch@in.tum.de> / hgweb
  69. remove SpecCheck; it is now part of the AFP — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb

#61 (Jul 18, 2021, 12:14:00 AM)

  1. compile — blanchet / hgweb
  2. more realistic timeout: 50min CPU time; — wenzelm / hgweb
  3. Minor changes to Finitely_Generated_Abelian_Groups, simplified and extended Dirichlet_L by depending
    on Finitely_Generated_Abelian_Groups — Joseph Thommes <joseph-thommes@gmx.de> / hgweb
  4. new entry Finitely_Generated_Abelian_Groups — paulson <lp15@cam.ac.uk> / hgweb
  5. remove duplicate entry in metadata — Lars Hupel <lars.hupel@mytum.de> / hgweb
  6. more coherent dependencies — haftmann / hgweb
  7. fix(Regex_Equivalence) update to new SpecCheck version — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
  8. operations for symbolic computation of bit operations — haftmann / hgweb
  9. fixed Proof_Strategy_Language following Isabelle/f58108b7a60c — desharna / hgweb
  10. SpecCheck now without _ (Regex_Equivalence is still broken) — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb

#60 (Jul 11, 2021, 12:14:00 AM)

  1. merged — desharna / hgweb
  2. added documentation for changes to Sledgehammer option "lam_trans" — desharna / hgweb
  3. jenkins: pre/post-hook results — Fabian Huch <huch@in.tum.de> / hgweb
  4. merged — desharna / hgweb
  5. added opaque_combs and renamed hide_lams to opaque_lifting — desharna / hgweb
  6. more robust treatment of empty string; — wenzelm / hgweb
  7. invoke Scala compiler from Java, without external process;
    tuned messages; — wenzelm / hgweb
  8. clarified version: Apple now counts like 11, 12, ...; — wenzelm / hgweb
  9. Imported lots of material from Stirling_Formula/Gamma_Asymptotics — paulson <lp15@cam.ac.uk> / hgweb

#60 (Jul 11, 2021, 12:14:00 AM)

  1. T1 fontenc for new entries — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  2. sitegen — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  3. update hide_lams -> opaque_lifting — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  4. merged from afp2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  5. website for SpecCheck — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  6. new entry SpecCheck — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  7. metadata and sitegen for MiniSail — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  8. new entry: MiniSail — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  9. sitegen for Public Announcement Logic — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  10. new entry "Public Announcement Logic"
    (and sorted ROOTS + removed duplicate entries in ROOTS) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  11. fixed a messy reference — paulson <lp15@cam.ac.uk> / hgweb
  12. Van_der_Waerden website — paulson <lp15@cam.ac.uk> / hgweb
  13. new entry Van_der_Waerden — paulson <lp15@cam.ac.uk> / hgweb
  14. New entry IMP_Compiler — nipkow / hgweb
  15. Removal of unintended files — Susannah Mansky <susannahej@gmail.com> / hgweb
  16. Hidden.thy to Isar — Susannah Mansky <susannahej@gmail.com> / hgweb
  17. merged — desharna / hgweb
  18. renamed hide_lams opaque_lifting — desharna / hgweb
  19. merged — Fabian Huch <huch@in.tum.de> / hgweb
  20. jenkins: pre/post-hook results — Fabian Huch <huch@in.tum.de> / hgweb
  21. changed to opaque_lifiting as suggested by Isabelle/Jenkins — yonoteam <jonjulian23@gmail.com> / hgweb
  22. changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins — yonoteam <jonjulian23@gmail.com> / hgweb
  23. Added missing Public_Announcement_Logic to ROOTS file — Manuel Eberl <eberlm@in.tum.de> / hgweb
  24. More Support on Clean Syntax, Basic Lens Support, New Examples. — Burkhart Wolff <wolff@lri.fr> / hgweb
  25. finishing arg -> Arg and moving some material out of Stirling_Formula/Gamma_Asymptotics — paulson <lp15@cam.ac.uk> / hgweb

#59 (Jul 4, 2021, 12:14:00 AM)

  1. merged — paulson / hgweb
  2. arg for the nonstandard complex numbers — paulson <lp15@cam.ac.uk> / hgweb
  3. merged — paulson / hgweb
  4. converting arg to Arg — paulson <lp15@cam.ac.uk> / hgweb
  5. just a bit of tidying up — paulson <lp15@cam.ac.uk> / hgweb
  6. create jar in pure Java; — wenzelm / hgweb
  7. tuned signature; — wenzelm / hgweb
  8. clarified order; — wenzelm / hgweb
  9. proper treatment of leading zero; — wenzelm / hgweb
  10. support for jar resources; — wenzelm / hgweb
  11. tuned whitespace; — wenzelm / hgweb
  12. tuned signature; — wenzelm / hgweb
  13. tuned; — wenzelm / hgweb
  14. support for Isabelle/Scala in pure Java; — wenzelm / hgweb
  15. tuned signature; — wenzelm / hgweb
  16. clarified directories; — wenzelm / hgweb
  17. clarified modules and signatures; — wenzelm / hgweb
  18. back to scala-2.13.5: avoid problems with history in scala REPL; — wenzelm / hgweb
  19. tuned imports; — wenzelm / hgweb
  20. merged — wenzelm / hgweb
  21. clarified Isabelle/Java/Scala project setup; — wenzelm / hgweb
  22. support for Isabelle setup in pure Java; — wenzelm / hgweb
  23. tuned: prefer Java interfaces; — wenzelm / hgweb
  24. clarified package: towards stand-alone setup; — wenzelm / hgweb
  25. tuned; — wenzelm / hgweb
  26. more direct java.home, according to current jdk directory layout; — wenzelm / hgweb
  27. tuned; — wenzelm / hgweb
  28. clarified modules;
    avoid initial use of _settings during init; — wenzelm / hgweb
  29. tuned: prefer Java interfaces; — wenzelm / hgweb
  30. tuned: prefer Java interfaces; — wenzelm / hgweb
  31. clarified signature: prefer Java interfaces; — wenzelm / hgweb
  32. clarified signature; — wenzelm / hgweb
  33. clarified signature; — wenzelm / hgweb
  34. proper usage; — wenzelm / hgweb
  35. clarified modules; — wenzelm / hgweb
  36. tuned; — wenzelm / hgweb
  37. clarified modules (again): services require full Isabelle/Scala environment; — wenzelm / hgweb
  38. clarified modules; — wenzelm / hgweb
  39. updated to scala-2.13.6, with scala-xml 1.3.0 ~> 2.0.0; — wenzelm / hgweb
  40. clarified environment (amending 9444489766a1); — wenzelm / hgweb
  41. merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  42. move code setup from Cardinality to separate theory — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  43. A few useful lemmas about derivatives, colinearity and other topics — paulson <lp15@cam.ac.uk> / hgweb

#59 (Jul 4, 2021, 12:14:00 AM)

  1. arg -> Arg: the last holdout — paulson <lp15@cam.ac.uk> / hgweb
  2. merged — paulson / hgweb
  3. arg -> Arg — paulson <lp15@cam.ac.uk> / hgweb
  4. Add entry public announcement logic — Asta Halkjær From <andro.from@gmail.com> / hgweb
  5. merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  6. adapt to changes in HOL-Library.Cardinality — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  7. Added Approximation_Algorithm for Center_Selection — nipkow / hgweb

#58 (Jun 27, 2021, 12:14:00 AM)

  1. proper Font_Subst.cache for paintScreenLineRange; — wenzelm / hgweb
  2. more predictable result, avoid slightly odd "lastSubstFont" by jEdit; — wenzelm / hgweb
  3. tuned; — wenzelm / hgweb
  4. tuned signature; — wenzelm / hgweb
  5. tuned; — wenzelm / hgweb
  6. discontinue i21of4 (old Apple hardware); — wenzelm / hgweb
  7. avoid deprecated operation; — wenzelm / hgweb
  8. tuned; — wenzelm / hgweb
  9. support for jEdit font substitution; — wenzelm / hgweb
  10. more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
    more direct TextAttribute.RUN_DIRECTION_LTR (see also ce22e5c3d4ce); — wenzelm / hgweb
  11. updated to flatlaf-1.2; — wenzelm / hgweb
  12. proper directories after reinstallation of lxbroy10; — wenzelm / hgweb
  13. more visual emphasis on node status; — wenzelm / hgweb
  14. more word cleanup — haftmann / hgweb
  15. merged — haftmann / hgweb
  16. more default simp rules — haftmann / hgweb
  17. some word streamlining — haftmann / hgweb
  18. avoid legacy domain informatik.tu-muenchen.de; — wenzelm / hgweb

#58 (Jun 27, 2021, 12:14:00 AM)

  1. proved conditional completeness of compilation — desharna / hgweb
  2. fixed typos — nipkow / hgweb
  3. more word cleanup — haftmann / hgweb
  4. more default simp rules — haftmann / hgweb
  5. some word streamlining — haftmann / hgweb
  6. made consistent again — haftmann / hgweb
  7. Fixed entry name for theories in sub-directory — Fabian Huch <huch@in.tum.de> / hgweb
  8. Stone_Relation_Algebras, Aggregation_Algebras: added history to metadata — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb

#57 (Jun 20, 2021, 12:14:00 AM)

  1. tuned --- following hints by IntelliJ; — wenzelm / hgweb
  2. tuned signature; — wenzelm / hgweb
  3. tuned; — wenzelm / hgweb
  4. tuned; — wenzelm / hgweb
  5. tuned signature; — wenzelm / hgweb
  6. tuned; — wenzelm / hgweb
  7. tuned signature (see 2d6a489adb01); — wenzelm / hgweb
  8. added support for TFX's and THF's $ite to Sledgehammer — desharna / hgweb
  9. tuned Mirabelle documentation — desharna / hgweb
  10. shortened long lines — desharna / hgweb
  11. fixed typos — desharna / hgweb
  12. updated Mirabelle documentation — desharna / hgweb
  13. changed Mirabelle's filter to use short theory names — desharna / hgweb
  14. more lemmas — haftmann / hgweb

#57 (Jun 20, 2021, 12:14:00 AM)

  1. Relational_Disjoint_Set_Forests: updated metadata to reflect added theory — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  2. Relational_Disjoint_Set_Forests: add theory More_Disjoint_Set_Forests — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  3. lemma grooming — haftmann / hgweb
  4. no duplicates of shift operations — haftmann / hgweb
  5. merge Jinja/Isar work — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  6. updated change history for Interpreter_Optimization — desharna / hgweb
  7. merged — paulson / hgweb
  8. updated, replacing axiomatizations by proper locales — paulson <lp15@cam.ac.uk> / hgweb
  9. added basic blocks — desharna / hgweb
  10. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  11. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  12. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  13. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  14. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  15. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  16. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  17. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  18. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  19. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  20. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  21. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  22. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  23. Merge from default, esp JinjaDCI — Susannah Mansky <susannahej@gmail.com> / hgweb
  24. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
  25. Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb

#56 (Jun 13, 2021, 12:14:59 AM)

  1. added support for unbounded max calls to Mirabelle — desharna / hgweb
  2. added warnings when defining unamed or redefining Mirabelle action — desharna / hgweb
  3. tuned whitespace; — wenzelm / hgweb
  4. tuned Mirabelle — desharna / hgweb
  5. merged — desharna / hgweb
  6. refactored Mirabelle to produce output in real time — desharna / hgweb
  7. global interpretation into nested targets — haftmann / hgweb
  8. more succint interfaces — haftmann / hgweb
  9. merged — wenzelm / hgweb
  10. tuned messages; — wenzelm / hgweb
  11. NEWS; — wenzelm / hgweb
  12. proper profiling within command execution: messages require PIDE id; — wenzelm / hgweb
  13. more systematic treatment of profiling mode; — wenzelm / hgweb
  14. tuned message; — wenzelm / hgweb
  15. prefer less intrusive tracing message; — wenzelm / hgweb
  16. clarified documentation: tracing messages are not shown here; — wenzelm / hgweb
  17. add missing file; — wenzelm / hgweb
  18. more formal ML profiling messages; — wenzelm / hgweb
  19. clarified modules; — wenzelm / hgweb
  20. Lukas Steven's more general fold foctions for maps — nipkow / hgweb
  21. More general fold function for maps — nipkow / hgweb
  22. follow Phabricator update 2021 Week 23; — wenzelm / hgweb
  23. tuned; — wenzelm / hgweb
  24. more formal theory and session names;
    tuned whitespace; — wenzelm / hgweb
  25. proper NEWS after Isabelle2021; — wenzelm / hgweb
  26. updated descriptions; — wenzelm / hgweb
  27. allow system option short form NAME for NAME=true for type string, not just bool;
    support short system options "-o document" and "-o system_log"; — wenzelm / hgweb
  28. tuned; — wenzelm / hgweb
  29. more robust within session "HOL"; — wenzelm / hgweb
  30. merged — wenzelm / hgweb
  31. suppress theories from other sessions, unless explicitly specified via mirabelle_theories; — wenzelm / hgweb
  32. clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT); — wenzelm / hgweb
  33. refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories; — wenzelm / hgweb
  34. tuned; — wenzelm / hgweb
  35. more uniform schedule_theories, notably for "present" and "commit" phase after loading; — wenzelm / hgweb
  36. tuned; — wenzelm / hgweb
  37. moved more legacy to AFP — haftmann / hgweb

#56 (Jun 13, 2021, 12:14:59 AM)

  1. Fix typo in date — Asta Halkjær From <andro.from@gmail.com> / hgweb
  2. Lukas Steven's changes for his fold updates — nipkow / hgweb
  3. moved more legacy to AFP — haftmann / hgweb
  4. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  5. suppress site-gen warning — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  6. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  7. exclude etc/ in afp_check_roots — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  8. strip trailing whitespace; make full URL — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  9. update usage instrucions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  10. more robust component setup for AFP/thys: support "isabelle components -u" and init $AFP_BASE on demand;
    no ROOTS in $AFP_BASE: proper support for "isabelle build -a" with $AFP_BASE component, but without $AFP component; — wenzelm / hgweb
  11. sitegen for Lifting_the_Exponent — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  12. new entry Lifting_the_Exponent — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb

#55 (Jun 6, 2021, 12:14:00 AM)

  1. clarified modules; — wenzelm / hgweb
  2. clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys); — wenzelm / hgweb
  3. tuned; — wenzelm / hgweb
  4. more thorough update of required files (amending 1529c3eb6bac); — wenzelm / hgweb
  5. clarified examples; — wenzelm / hgweb
  6. tuned proofs; — wenzelm / hgweb
  7. misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a); — wenzelm / hgweb
  8. tuned --- reduced source complexity; — wenzelm / hgweb
  9. proper usage (amending f7ea394490f5); — wenzelm / hgweb
  10. merged, resolving minor conflict; — wenzelm / hgweb
  11. allow build session setup, e.g. for protocol handlers; — wenzelm / hgweb
  12. unused; — wenzelm / hgweb
  13. tuned --- potentially more robust (e.g. session.phase_changed vs. isabelle_process.terminated); — wenzelm / hgweb
  14. clarified signature; — wenzelm / hgweb
  15. removed pointless option (see 3d0952893db8); — wenzelm / hgweb
  16. tuned --- avoid redundant future tasks from already loaded theories; — wenzelm / hgweb
  17. no comment --- topological order appears to be fine since 04-Mar-2013; — wenzelm / hgweb
  18. more predictable sequential presentation (2f9877db82a1), without somewhat pointless result_ord (e7fab0b5dbe7); — wenzelm / hgweb
  19. moved stride option from sledgehammer action to main mirabelle — desharna / hgweb
  20. merged — paulson / hgweb
  21. new lemmas mostly about paths — paulson <lp15@cam.ac.uk> / hgweb
  22. lexorders the locale way — haftmann / hgweb
  23. more accurate export morphism enables proper instantiation by interpretation — haftmann / hgweb

#55 (Jun 6, 2021, 12:14:00 AM)

  1. more specific export_files: omit recent additions ("document", "PIDE", etc.); — wenzelm / hgweb
  2. grouped lemmas — haftmann / hgweb
  3. bundles for traditional infix syntax — haftmann / hgweb

#54 (May 30, 2021, 12:14:00 AM)

  1. merged — paulson / hgweb
  2. some new and/or varient results about images — paulson <lp15@cam.ac.uk> / hgweb
  3. nicer statement of Liouville_theorem — paulson <lp15@cam.ac.uk> / hgweb
  4. more lemmas — haftmann / hgweb
  5. max word moved to Word_Lib in AFP — haftmann / hgweb
  6. more robust syntax; — wenzelm / hgweb
  7. unused; — wenzelm / hgweb
  8. clarified document export names; — wenzelm / hgweb
  9. tuned signature; — wenzelm / hgweb
  10. tuned; — wenzelm / hgweb
  11. tuned; — wenzelm / hgweb
  12. avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac; — wenzelm / hgweb
  13. compose Latex text as XML, output exported YXML in Isabelle/Scala; — wenzelm / hgweb
  14. more direct index_entry: no positions required -- text is eventually moved to .ind file; — wenzelm / hgweb
  15. clarified signature; — wenzelm / hgweb
  16. clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle"); — wenzelm / hgweb
  17. tuned message, e.g. for Pure bootstrap; — wenzelm / hgweb
  18. proper signature export (amending b50f8cc8c08e); — wenzelm / hgweb
  19. syslog option for "isabelle build"; — wenzelm / hgweb
  20. further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea); — wenzelm / hgweb
  21. merged — wenzelm / hgweb
  22. NEWS; — wenzelm / hgweb
  23. clarified index, more like formal @{element_ref}; — wenzelm / hgweb
  24. clarified treatment of type constructors; — wenzelm / hgweb
  25. misc tuning and clarification; — wenzelm / hgweb
  26. tuned signature; — wenzelm / hgweb
  27. clarified context; — wenzelm / hgweb
  28. more uniform document antiquotations for ML: consolidate former setup for manuals; — wenzelm / hgweb
  29. clarified names; — wenzelm / hgweb
  30. clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax; — wenzelm / hgweb
  31. clarified modules; — wenzelm / hgweb
  32. clarified modules; — wenzelm / hgweb
  33. tuned; — wenzelm / hgweb
  34. clarified signature: avoid dispatch via name; — wenzelm / hgweb
  35. clarified, e.g. type variables; — wenzelm / hgweb
  36. tuned index; — wenzelm / hgweb
  37. more ambitious default for index "is like"; — wenzelm / hgweb
  38. tuned; — wenzelm / hgweb
  39. support for index entries; — wenzelm / hgweb
  40. tuned; — wenzelm / hgweb
  41. tuned signature; — wenzelm / hgweb
  42. clarified modules; — wenzelm / hgweb
  43. clarified old document build; — wenzelm / hgweb
  44. unused; — wenzelm / hgweb
  45. prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been removed already in 435fb018e8ee; — wenzelm / hgweb
  46. prefer standard document_build=lualatex --- no impact of "sedindex" in prepare_document; — wenzelm / hgweb
  47. unused; — wenzelm / hgweb
  48. proper Unix lines; — wenzelm / hgweb
  49. prefer explicit option document_bibliography (actually ignored by build script); — wenzelm / hgweb
  50. explicit option document_bibliography; — wenzelm / hgweb
  51. proper bibliography; — wenzelm / hgweb
  52. discontinued obsolete "isabelle latex"; — wenzelm / hgweb
  53. more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
    clarified ISABELLE_MAKEINDEX options; — wenzelm / hgweb
  54. default document_build (lualatex); — wenzelm / hgweb
  55. more robust: allow \printindex within the document; — wenzelm / hgweb
  56. clarified bash scripts, with public interfaces for user-defined Document_Build.Engine; — wenzelm / hgweb
  57. tuned signature; — wenzelm / hgweb
  58. option document_preprocessor; — wenzelm / hgweb
  59. show symbols in Isabelle/ML instead of perl; — wenzelm / hgweb
  60. more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; — wenzelm / hgweb
  61. tuned --- more robust; — wenzelm / hgweb
  62. discontinued somewhat pointless "fixbookmarks": default output works sufficiently well; — wenzelm / hgweb
  63. more uniform bibtex error, without using perl (see 4710dd5093a3); — wenzelm / hgweb
  64. proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error); — wenzelm / hgweb
  65. tuned; — wenzelm / hgweb
  66. clarified command-line options; — wenzelm / hgweb
  67. obsolete (see 5a3a2a52648d); — wenzelm / hgweb
  68. redundant: copy produced from session document_files; — wenzelm / hgweb
  69. clarified treatment of Isabelle .sty files; — wenzelm / hgweb
  70. option document_logo; — wenzelm / hgweb
  71. proper options; — wenzelm / hgweb
  72. option document_build refers to build engine in Isabelle/Scala;
    pdflatex is back as legacy build engine, e.g. for published proceedings; — wenzelm / hgweb
  73. redundant: tmp_dir is purged anyway; — wenzelm / hgweb
  74. misc tuning and clarification; — wenzelm / hgweb
  75. clarified modules; — wenzelm / hgweb
  76. tuned --- clarified corner cases; — wenzelm / hgweb
  77. more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases; — wenzelm / hgweb
  78. clarified signature -- avoid odd warning about scala/bug#6675; — wenzelm / hgweb
  79. tuned; — wenzelm / hgweb
  80. tuned; — wenzelm / hgweb
  81. clarified signature; — wenzelm / hgweb
  82. proper syntax of Scala 3; — wenzelm / hgweb
  83. enforce syntax of Scala 3; — wenzelm / hgweb

#54 (May 30, 2021, 12:14:00 AM)

  1. complement reduced to mere abbreviation — haftmann / hgweb
  2. extracted more legacy abbreviations — haftmann / hgweb
  3. max word moved to Word_Lib in AFP — haftmann / hgweb
  4. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  5. update website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  6. fix links — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  7. Restore deleted theorem from Szpilrajn — Lukas Stevens <mail@lukas-stevens.de> / hgweb
  8. tuned presentation — haftmann / hgweb
  9. adapted to devel — nipkow / hgweb
  10. adjusted to changes in distribution — haftmann / hgweb
  11. adjust Combinatorics_Words to isabelle@493b1ae188da — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  12. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  13. make AFP ROOTS globally available for component — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  14. merged — nipkow / hgweb
  15. New entries Combinatorics_Words* — nipkow / hgweb
  16. adjusted to change in distribution — haftmann / hgweb
  17. adapted to Isabelle/466fae6bf22e; — wenzelm / hgweb
  18. tuned whitespace; — wenzelm / hgweb
  19. Remove comment about missing refinement — n.muendler <n.muendler@tum.de> / hgweb
  20. continued uglification, but also fixed some dodgy proofs — paulson <lp15@cam.ac.uk> / hgweb
  21. fixed some broken / looping / fragile proofs — paulson <lp15@cam.ac.uk> / hgweb
  22. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  23. simplify usage instructions more — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  24. sitegen for Padic_Ints — Manuel Eberl <eberlm@in.tum.de> / hgweb
  25. new entry: Padic_Ints — Manuel Eberl <eberlm@in.tum.de> / hgweb
  26. update affiliation — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  27. New entry: Regressioon_Test_Selection — nipkow / hgweb
  28. metadata for Metalogic_ProofChecker — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  29. new entry Metalogic_ProofChecker — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  30. metadata for GaleStewart_Games — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  31. new entry GaleStewart_Games — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  32. fixed the ROOT file ofr BenOr_Kozen_Reif — paulson <lp15@cam.ac.uk> / hgweb
  33. webpage for BenOr_Kozen_Reif — paulson <lp15@cam.ac.uk> / hgweb
  34. new entry BenOr_Kozen_Reif — paulson <lp15@cam.ac.uk> / hgweb
  35. Slight tidying to shorten too-long lines — paulson <lp15@cam.ac.uk> / hgweb
  36. added a necessary acknowledgment (ERC) — paulson <lp15@cam.ac.uk> / hgweb
  37. New entry Progress_Tracking — nipkow / hgweb
  38. Revisions by Wenda to eliminate the locale comp_affine_scheme — paulson <lp15@cam.ac.uk> / hgweb
  39. renamed a lemma — paulson <lp15@cam.ac.uk> / hgweb
  40. Fixed an error in the statement of closed_subsets_empty. Also added syntax priority hints for carrier_of_local_ring_at. — paulson <lp15@cam.ac.uk> / hgweb
  41. consolidated metadata of Anthony Bordg, metadata for new Grothendieck entry + sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  42. new entry: Grothendieck_Schemes — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  43. metadata for IFC_Tracking — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  44. new entry IFC_Tracking — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  45. merged — wenzelm / hgweb
  46. adapted to Isabelle/ef1a18e20ace; — wenzelm / hgweb
  47. recover some patches after years of continuously changing Isabelle LaTeX output; — wenzelm / hgweb
  48. prefer document_preprocessor over document_build; — wenzelm / hgweb
  49. prefer document_logo instead of document_build script; — wenzelm / hgweb
  50. proper options; — wenzelm / hgweb

#53 (May 23, 2021, 12:14:00 AM)

  1. things need to be ugly — paulson <lp15@cam.ac.uk> / hgweb
  2. merged — paulson / hgweb
  3. sorted as an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
  4. mere abbreviation for logical alias — haftmann / hgweb
  5. avoid unexpected output+behaviour when CDPATH is set — kleing / hgweb
  6. recover some Linux test, using old macbroy2 as i21of4 (Ubuntu 20.04); — wenzelm / hgweb
  7. avoid perl; — wenzelm / hgweb
  8. tuned signature --- following hints by IntelliJ IDEA; — wenzelm / hgweb
  9. ignore session build timeout, notably in AFP; — wenzelm / hgweb
  10. check timeout_ignored as in ML, before applying timeout_scale; — wenzelm / hgweb
  11. merged — wenzelm / hgweb
  12. proper build of required session images vs. build with Mirabelle presentation; — wenzelm / hgweb
  13. reactive "sledgehammer"; — wenzelm / hgweb
  14. reactive "sledgehammer_filter": statically correct, but untested (no proof_file); — wenzelm / hgweb
  15. clarified command-line; — wenzelm / hgweb
  16. clarified signature;
    supporess empty results; — wenzelm / hgweb
  17. clarified signature; — wenzelm / hgweb
  18. clarified log content; — wenzelm / hgweb
  19. reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; — wenzelm / hgweb
  20. tuned; — wenzelm / hgweb
  21. unused; — wenzelm / hgweb
  22. unused (see 8ffc607c345d); — wenzelm / hgweb
  23. clarified signature: provide access to previous state; — wenzelm / hgweb
  24. clarified signature (see Scala version); — wenzelm / hgweb
  25. tuned signature; — wenzelm / hgweb
  26. avoid duplicate loading of ML file; — wenzelm / hgweb

#53 (May 23, 2021, 12:14:00 AM)

  1. PATCH to Auto2 (for sorted) by Bohua, pending a permanent generalisation of "properties" — paulson <lp15@cam.ac.uk> / hgweb
  2. fixed two more "sorted" errors — paulson <lp15@cam.ac.uk> / hgweb
  3. fixed two "sorted" issues — paulson <lp15@cam.ac.uk> / hgweb
  4. merged — paulson / hgweb
  5. changes for "sorted" as an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
  6. mere abbreviation for logical alias — haftmann / hgweb
  7. eliminated odd clone (see Isabelle/caa5a257d3ed); — wenzelm / hgweb

#52 (May 16, 2021, 12:14:00 AM)

  1. strict_sorted now an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
  2. explicit type class operations for type-specific implementations — haftmann / hgweb
  3. obsolete — haftmann / hgweb
  4. added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran — desharna / hgweb
  5. merged — nipkow / hgweb
  6. generalized type — nipkow / hgweb
  7. basic setup of Isabelle setup tool --- pure Java, no dependencies; — wenzelm / hgweb
  8. merged — wenzelm / hgweb
  9. guess package more directly; — wenzelm / hgweb
  10. merged — paulson / hgweb
  11. Just one lemma — paulson <lp15@cam.ac.uk> / hgweb
  12. proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64; — wenzelm / hgweb
  13. clarified platforms; — wenzelm / hgweb
  14. merged — wenzelm / hgweb
  15. proper jEdit.props (amending ff716ecb0805); — wenzelm / hgweb
  16. update to gmp-6.2.1, with support for arm64-darwin; — wenzelm / hgweb
  17. clarified platforms; — wenzelm / hgweb
  18. clarified options: implicitly support both x86_64 and arm64; — wenzelm / hgweb
  19. tuned whitespace; — wenzelm / hgweb
  20. centralized more lemmas — haftmann / hgweb
  21. avoid Fun.swap — haftmann / hgweb
  22. guide is out of focus — haftmann / hgweb
  23. proper build for fresh target directory (amending d9823224fcfe); — wenzelm / hgweb
  24. put more resources into jedit_build component; — wenzelm / hgweb
  25. more brackets (see f6b453449cc6); — wenzelm / hgweb
  26. more brackets; — wenzelm / hgweb
  27. proper settings variable, amending 6e85281177df; — wenzelm / hgweb
  28. merged — wenzelm / hgweb
  29. tuned proofs --- avoid z3, which is absent on arm64-linux; — wenzelm / hgweb
  30. proper condition: z3 could be absent, e.g. on arm64-linux; — wenzelm / hgweb
  31. build auxiliary jEdit component in Isabelle/Scala;
    clarified directory layout; — wenzelm / hgweb
  32. separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597); — wenzelm / hgweb
  33. tuned message; — wenzelm / hgweb
  34. clarified signature; — wenzelm / hgweb
  35. tuned signature; — wenzelm / hgweb
  36. more elementary swap — haftmann / hgweb

#52 (May 16, 2021, 12:14:00 AM)

  1. strict_sorted now an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
  2. merged — paulson / hgweb
  3. deleted needless material — paulson <lp15@cam.ac.uk> / hgweb
  4. explicit type class operations for type-specific implementations — haftmann / hgweb
  5. next step to phase out ancient numerals — haftmann / hgweb
  6. more small simplifications — paulson <lp15@cam.ac.uk> / hgweb
  7. merged — paulson / hgweb
  8. fixed some latex; tried the alternative definition of Ramsey — paulson <lp15@cam.ac.uk> / hgweb
  9. Trying out Ramsey_eq for simpler proofs — paulson <lp15@cam.ac.uk> / hgweb
  10. more tiny tweaks — paulson <lp15@cam.ac.uk> / hgweb
  11. centralized more lemmas — haftmann / hgweb
  12. avoid Fun.swap — haftmann / hgweb
  13. guide is out of focus — haftmann / hgweb
  14. Relational_Minimum_Spanning_Trees: refactoring Boruvka.thy — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
  15. more elementary swap — haftmann / hgweb

#49 (Apr 25, 2021, 12:14:00 AM)

  1. collecting more lemmas concerning multisets — haftmann / hgweb

#49 (Apr 25, 2021, 12:14:00 AM)

  1. collecting more lemmas concerning multisets — haftmann / hgweb

#47 (Apr 21, 2021, 10:29:10 AM)

  1. proper use of antiquotations; — wenzelm / hgweb
  2. more documentation on "Conversions"; — wenzelm / hgweb
  3. tuned — nipkow / hgweb
  4. updated example; — wenzelm / hgweb
  5. clarified options (again); — wenzelm / hgweb
  6. more options: update ISABELLE_IDENTIFIER; — wenzelm / hgweb
  7. clarified conditional ML; — wenzelm / hgweb
  8. support for conditional ML text; — wenzelm / hgweb
  9. updated example; — wenzelm / hgweb
  10. clarified options; — wenzelm / hgweb
  11. proper context variable handling when stripping leadings quantifiers from test goals — haftmann / hgweb
  12. proper etc/ISABELLE_ID from archive (amending 4cba4e250c28); — wenzelm / hgweb
  13. eliminated perl: prefer elementary GNU printenv; — wenzelm / hgweb
  14. more robust bootstrap of components; — wenzelm / hgweb
  15. more self-contained support for macOS; — wenzelm / hgweb
  16. misc tuning and clarification; — wenzelm / hgweb
  17. tuned signature; — wenzelm / hgweb
  18. support for base64 via Isabelle/Scala/ML; — wenzelm / hgweb
  19. compile; — wenzelm / hgweb
  20. clarified signature: avoid overlap of String vs. Bytes (both are CharSequence); — wenzelm / hgweb
  21. clarified signature (again); — wenzelm / hgweb
  22. merged — wenzelm / hgweb
  23. clarified signature; — wenzelm / hgweb
  24. unused; — wenzelm / hgweb
  25. unused; — wenzelm / hgweb
  26. clarified signature: more structured arguments, notably for remote provers; — wenzelm / hgweb
  27. clarified signature; — wenzelm / hgweb
  28. clarified signature: avoid tmp file; — wenzelm / hgweb
  29. clarified signature for Scala functions; — wenzelm / hgweb
  30. clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9); — wenzelm / hgweb
  31. tuned; — wenzelm / hgweb
  32. clarified cache; — wenzelm / hgweb
  33. clarified signature: Bytes extends CharSequence already (see d201996f72a8); — wenzelm / hgweb
  34. clarified exceptions; — wenzelm / hgweb
  35. more uniform use of Byte_Message;
    support protocol_message with multiple chunks; — wenzelm / hgweb
  36. tuned signature; — wenzelm / hgweb
  37. tuned signature; — wenzelm / hgweb
  38. more robust treatment of empty markup: it allows to produce formal chunks; — wenzelm / hgweb
  39. collected combinatorial material — haftmann / hgweb
  40. tuned; — wenzelm / hgweb
  41. tuned; — wenzelm / hgweb
  42. more documentation; — wenzelm / hgweb
  43. proper treatment of nested antiquotations;
    clarified signature; — wenzelm / hgweb
  44. support for ML special forms: modified evaluation similar to Scheme; — wenzelm / hgweb
  45. clarified signature: more detailed token positions for antiquotations; — wenzelm / hgweb
  46. merged — wenzelm / hgweb
  47. clarified signature; — wenzelm / hgweb
  48. confluent preprocessing for floats in presence of target language numerals — haftmann / hgweb
  49. subclass relation — haftmann / hgweb
  50. some tinkering with npm versions; — wenzelm / hgweb
  51. some tinkering with npm versions; — wenzelm / hgweb
  52. back to post-release mode; — wenzelm / hgweb
  53. tuned signature; — wenzelm / hgweb
  54. auto-update due to "isabelle build_vscode"; — wenzelm / hgweb
  55. tuned; — wenzelm / hgweb
  56. tuned --- following hints by IntelliJ IDEA; — wenzelm / hgweb
  57. fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes) — Manuel Eberl <eberlm@in.tum.de> / hgweb
  58. simplified definition — haftmann / hgweb
  59. new lemmas — haftmann / hgweb
  60. discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog-prove"; — wenzelm / hgweb
  61. following recent Phabricator update, after 2021 Week 13 (Late March); — wenzelm / hgweb
  62. merged — paulson / hgweb
  63. Cosmetic: no !! in the lemma statement — paulson <lp15@cam.ac.uk> / hgweb
  64. clarified README;
    avoid odd patching of sources; — wenzelm / hgweb
  65. more standard header, with utf-8 encoding; — wenzelm / hgweb
  66. clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources; — wenzelm / hgweb
  67. merged — nipkow / hgweb
  68. new automatic order prover: stateless, complete, verified — nipkow / hgweb
  69. clarified signature; — wenzelm / hgweb
  70. clarified: follow "isabelle version -t"; — wenzelm / hgweb
  71. further clarification of Isabelle distribution identification -- avoid odd patching of sources; — wenzelm / hgweb
  72. tuned signature -- more explicit types; — wenzelm / hgweb
  73. more robust and uniform ISABELLE_TAGS; — wenzelm / hgweb
  74. clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos; — wenzelm / hgweb
  75. simplified release status (again), in contrast to a43898f76ae9; — wenzelm / hgweb
  76. more uniform HTTP resources; — wenzelm / hgweb
  77. clarified (again): local tip could be actually more recent; — wenzelm / hgweb
  78. tuned; — wenzelm / hgweb
  79. tuned; — wenzelm / hgweb
  80. clarified name; — wenzelm / hgweb
  81. more systematic java_library: avoid empty entries, declaration order as for other bash functions; — wenzelm / hgweb
  82. support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.; — wenzelm / hgweb
  83. updated to latest latex due to new mechanism for dealing with bold ccfonts — nipkow / hgweb
  84. removal of needless hypothesis in hd_rev and last_rev — paulson <lp15@cam.ac.uk> / hgweb

#47 (Apr 21, 2021, 10:29:10 AM)

  1. more realistic timeout; — wenzelm / hgweb
  2. tuned whitespace; — wenzelm / hgweb
  3. Tweaks — Asta Halkjær From <andro.from@gmail.com> / hgweb
  4. adapted to Isabelle/a2c589d5e1e4; — wenzelm / hgweb
  5. Merge — paulson <lp15@cam.ac.uk> / hgweb
  6. tweak — paulson <lp15@cam.ac.uk> / hgweb
  7. simplified proof — nipkow / hgweb
  8. sshiftr/bl lemmas by Florian Märkl — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  9. proof simplification — paulson <lp15@cam.ac.uk> / hgweb
  10. cosmetic tweaks to proofs — paulson <lp15@cam.ac.uk> / hgweb
  11. merged — paulson / hgweb
  12. minor stylistic changes — paulson <lp15@cam.ac.uk> / hgweb
  13. Add completeness of modal logics T, KB, K4, S4 and S5 — Asta Halkjær From <andro.from@gmail.com> / hgweb
  14. Stylistic tweaks, which I hope are improvements :-) — paulson <lp15@cam.ac.uk> / hgweb
  15. updated paper references — traytel / hgweb
  16. merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  17. increased timeout — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  18. collected combinatorial material — haftmann / hgweb
  19. Update root.tex — Asta Halkjær From <andro.from@gmail.com> / hgweb
  20. Cut out Fitting's consistency properties — Asta Halkjær From <andro.from@gmail.com> / hgweb
  21. fixed proof — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  22. clarified message, following Isabelle/a7aabdf889b7; — wenzelm / hgweb
  23. confluent preprocessing for floats in presence of target language numerals — haftmann / hgweb
  24. subclass relation — haftmann / hgweb
  25. adapted to isabelle-dev/56db8559eadb — Manuel Eberl <eberlm@in.tum.de> / hgweb
  26. simplified definition — haftmann / hgweb
  27. new lemmas — haftmann / hgweb
  28. probable fix suggested by Cornelius for the changes in the vicinity of 2cd23d587db9 — nipkow / hgweb
  29. Fixes due to new order prover — nipkow / hgweb
  30. another broken proof — paulson <lp15@cam.ac.uk> / hgweb
  31. Fixed and simplified some failing proofs — paulson <lp15@cam.ac.uk> / hgweb
  32. Writing less_sets as an infix — paulson <lp15@cam.ac.uk> / hgweb
  33. avoid symblinks --- make it work on Windows; — wenzelm / hgweb
  34. Fixed some looping proofs (though why they were looping isn't clear) — paulson <lp15@cam.ac.uk> / hgweb
  35. Fixed a failing proof — paulson <lp15@cam.ac.uk> / hgweb
  36. merged — paulson / hgweb
  37. fixes for new hd_rev and last_rev — paulson <lp15@cam.ac.uk> / hgweb

#42 (Apr 4, 2021, 12:14:00 AM)

  1. more robust; — wenzelm / hgweb
  2. clarified message; — wenzelm / hgweb
  3. tuned; — wenzelm / hgweb
  4. tuned message; — wenzelm / hgweb
  5. proper export; — wenzelm / hgweb
  6. more options: build is part of default setup; — wenzelm / hgweb
  7. misc tuning and clarification; — wenzelm / hgweb
  8. more options; — wenzelm / hgweb
  9. proper Admin script, outside the settings environment; — wenzelm / hgweb
  10. tuned whitespace; — wenzelm / hgweb

#42 (Apr 4, 2021, 12:14:00 AM)

  1. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  2. Infix notation for the less_sets relation — paulson <lp15@cam.ac.uk> / hgweb
  3. merged — paulson / hgweb
  4. simplified a few proofs — paulson <lp15@cam.ac.uk> / hgweb
  5. sitegen and metadata for Constructive_Cryptography_CM — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  6. new entry Constructive_Cryptography_CM — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb

#41 (Mar 28, 2021, 12:14:00 AM)

  1. tuned; — wenzelm / hgweb
  2. clarified; — wenzelm / hgweb
  3. tuned message; — wenzelm / hgweb
  4. tuned message; — wenzelm / hgweb
  5. more accurate settings after update of current version; — wenzelm / hgweb
  6. clarified messages; — wenzelm / hgweb
  7. more robust: lest hg work out remote tip;
    more options; — wenzelm / hgweb
  8. more options; — wenzelm / hgweb
  9. clarified treatment of multiple versions: last one counts;
    more options; — wenzelm / hgweb
  10. more robust; — wenzelm / hgweb
  11. more robust: explicit repository root; — wenzelm / hgweb
  12. more robust; — wenzelm / hgweb
  13. more convenient repository setup; — wenzelm / hgweb
  14. tuned; — wenzelm / hgweb
  15. more robust invocation of hg; — wenzelm / hgweb
  16. more robust: idempotent; — wenzelm / hgweb
  17. more robust invocation of hg; — wenzelm / hgweb
  18. tuned; — wenzelm / hgweb
  19. clarified output;
    more options; — wenzelm / hgweb
  20. support repository archives (without full .hg directory); — wenzelm / hgweb
  21. more robust invocation of hg; — wenzelm / hgweb
  22. record official releases that follow a certain structure, with public access via https://isabelle.sketis.net/repos/isabelle/raw-file/tip/Admin/Release/official (NB: Isabelle2013-1 had to be retracted); — wenzelm / hgweb
  23. dedicated session for combinatorial material — haftmann / hgweb
  24. support for Java Chromium Embedded Framework (JCEF): still somewhat fragile; — wenzelm / hgweb
  25. enforce full build; — wenzelm / hgweb
  26. turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont; — wenzelm / hgweb
  27. discontinue fragile check in LaTeX, e.g. problems with toc entries; — wenzelm / hgweb
  28. merged — paulson / hgweb
  29. merged — paulson / hgweb
  30. type class relaxation — paulson <lp15@cam.ac.uk> / hgweb
  31. more NEWS; — wenzelm / hgweb
  32. clarified group (but hard to tell); — wenzelm / hgweb
  33. more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd;
    corresponding symbols and latex macros; — wenzelm / hgweb
  34. more lemmas — haftmann / hgweb
  35. clarified package name (actually both pxfonts and txfonts exist and have this font); — wenzelm / hgweb
  36. tuned; — wenzelm / hgweb
  37. prefer isabelle bbbfont; — wenzelm / hgweb
  38. enforce full build; — wenzelm / hgweb
  39. clarified symbol names, notably relevant for Z_Notation; — wenzelm / hgweb
  40. update README (actually after update of component); — wenzelm / hgweb
  41. high-quality blackboard-bold fonts from "txmia" (package "txfonts"); — wenzelm / hgweb

#41 (Mar 28, 2021, 12:14:00 AM)

  1. more robust invocation of hg; — wenzelm / hgweb
  2. Update tile to match metadata — Lukas Stevens <mail@lukas-stevens.de> / hgweb
  3. Extend entry Szpilrajn — Lukas Stevens <mail@lukas-stevens.de> / hgweb
  4. dedicated session for combinatorial material — haftmann / hgweb
  5. more lemmas — haftmann / hgweb

#40 (Mar 21, 2021, 12:14:00 AM)

  1. publish component; — wenzelm / hgweb
  2. further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster; — wenzelm / hgweb
  3. clarified \<Zcomp> (small) vs. \<Zsemi> (big); — wenzelm / hgweb
  4. more CONTRIBUTORS; — wenzelm / hgweb
  5. more Z_Notation symbols, as proposed by Simon Foster;
    some LaTeX-art based on tex.stackexchange "How do you make a square element symbol (\in)"; — wenzelm / hgweb
  6. more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the "minus"; — wenzelm / hgweb
  7. clarified order for GUI panel; — wenzelm / hgweb
  8. prefer more direct interpretation — haftmann / hgweb
  9. more Z_Notation symbols, as proposed by Simon Foster; — wenzelm / hgweb
  10. more accurate spacing, according to results seen in isar-ref (Appendix B), using 12pt or 10pt; — wenzelm / hgweb
  11. clarified order for presentation in isar-ref (Appendix B); — wenzelm / hgweb
  12. prefer explicit \<Zproject> (with its own Unicode codepoint); — wenzelm / hgweb
  13. more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
    NB: no bold version of 0x2900 due to fontforge crash "Internal Error: Some fragments did not join"; — wenzelm / hgweb
  14. tuned message; — wenzelm / hgweb
  15. proper directory of settings file;
    tuned; — wenzelm / hgweb
  16. tuned lemma — nipkow / hgweb
  17. added lemma — nipkow / hgweb
  18. tuned signature; — wenzelm / hgweb
  19. tuned signature (again); — wenzelm / hgweb
  20. tuned --- following hints by IntelliJ; — wenzelm / hgweb
  21. tuned comments; — wenzelm / hgweb
  22. proper shell quote; — wenzelm / hgweb
  23. removed spurious references to perl / libwww-perl; — wenzelm / hgweb
  24. invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
    clarified inlined command-line;
    clarified errors: exception ERROR becomes UnknownError (it could stem from Scala function); — wenzelm / hgweb
  25. clarified signature: refer to file name instead of file content; — wenzelm / hgweb
  26. compile; — wenzelm / hgweb
  27. clarified signature: more explicit types; — wenzelm / hgweb
  28. support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp; — wenzelm / hgweb
  29. clarified signature; — wenzelm / hgweb
  30. elapsed time to download content (and for the server to provide content); — wenzelm / hgweb
  31. more direct elapsed run_time via bash_process wrapper (via Scala and C); — wenzelm / hgweb

#40 (Mar 21, 2021, 12:14:00 AM)

  1. neater proof — paulson <lp15@cam.ac.uk> / hgweb
  2. merged — paulson / hgweb
  3. Removal of an unused theorem. Plus lots of white space — paulson <lp15@cam.ac.uk> / hgweb
  4. switch new entries' documents to T1 encoding — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  5. merge from afp-2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  6. corrected metadata (use acute's in names of J. Divasón and René T.) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
  7. sitegen for Modular_arithmetic_LLL_and_HNF_algorithms — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  8. metadata for Modular_arithmetic_LLL_and_HNF_algorithms — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  9. new entry Modular_arithmetic_LLL_and_HNF_algorithms — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  10. a slight streamlining — paulson <lp15@cam.ac.uk> / hgweb
  11. Hermite_Lindemann website — paulson <lp15@cam.ac.uk> / hgweb
  12. new entry Hermite_Lindemann — paulson <lp15@cam.ac.uk> / hgweb
  13. cosmetic changes — paulson <lp15@cam.ac.uk> / hgweb
  14. Projective_Measurements website — paulson <lp15@cam.ac.uk> / hgweb
  15. Projective_Measurements with files — paulson <lp15@cam.ac.uk> / hgweb
  16. new entry Projective_Measurements — paulson <lp15@cam.ac.uk> / hgweb
  17. add Andreas Lochbihler as editor — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  18. New entry: Mereology — nipkow / hgweb
  19. New entry Sunflowers — nipkow / hgweb
  20. refactored and added lemma state_behaves_forward_to_backward — desharna / hgweb

#39 (Mar 14, 2021, 12:14:00 AM)

  1. merged — wenzelm / hgweb
  2. use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages; — wenzelm / hgweb
  3. clarified signature: let Sledgehammer handle SystemOnTPTP comments; — wenzelm / hgweb
  4. clarified signature: url may change dynamically and is part of result; — wenzelm / hgweb
  5. clarified error; — wenzelm / hgweb
  6. support timeout, similar to perl LWP::UserAgent; — wenzelm / hgweb
  7. clarified signature; — wenzelm / hgweb
  8. tuned; — wenzelm / hgweb
  9. clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML; — wenzelm / hgweb
  10. support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl); — wenzelm / hgweb
  11. clarified HTTP.Content: support encoding;
    more realistic HTTP.Client operations; — wenzelm / hgweb
  12. clarified signature: more explicit HTTP operations; — wenzelm / hgweb
  13. tuned; — wenzelm / hgweb
  14. more robust; — wenzelm / hgweb
  15. clarified signature; — wenzelm / hgweb
  16. clarified components; — wenzelm / hgweb
  17. avoid name clash — haftmann / hgweb
  18. lemma — haftmann / hgweb
  19. tuned; — wenzelm / hgweb
  20. another example for lift_bnf for quotients — traytel / hgweb
  21. merged — wenzelm / hgweb
  22. proper \usepackage[T1]{fontenc}; — wenzelm / hgweb
  23. more robust init: avoid spilling opam artifacts; — wenzelm / hgweb
  24. proper type-setting of cartouches (requires T1);
    \usepackage[T1]{fontenc} is default for mkroot;
    \usepackage[utf8]{inputenc} is obsolete in lualatex; — wenzelm / hgweb
  25. provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04; — wenzelm / hgweb
  26. more robust;
    eliminated perl; — wenzelm / hgweb
  27. removed unused latex packages; — wenzelm / hgweb
  28. obsolete (see 0c837beeb5e7); — wenzelm / hgweb
  29. proper Isabelle/Scala tool --- avoid perl; — wenzelm / hgweb
  30. generalized confluence-based subdistributivity theorem for quotients;
    new example that triggered the generalization — traytel / hgweb
  31. Backed out changeset 3fdb94d87e0e — desharna / hgweb
  32. Backed out changeset b867b436f372 — desharna / hgweb
  33. reduced dependencies on List_Permutation — haftmann / hgweb
  34. follow corresponding precedence on sets — haftmann / hgweb
  35. consolidated names — haftmann / hgweb
  36. reduced dependencies on theory List_Permutation — haftmann / hgweb

#39 (Mar 14, 2021, 12:14:00 AM)

  1. avoid name clash — haftmann / hgweb
  2. adapted to LuaLaTeX according to Isabelle/299f6a8faccc;
    \usepackage[T1]{fontenc} is default, it provides e.g. proper cartouche-delimiters;
    \usepackage{lmodern} is no longer required, since T1 in LuaLaTeX has proper scalable fonts;
    \usepackage[utf8]{inputenc} is obsolete in LuaLaTeX;
    tuned whitespace; — wenzelm / hgweb
  3. reduced dependencies on List_Permutation — haftmann / hgweb
  4. follow corresponding precedence on sets — haftmann / hgweb
  5. consolidated names — haftmann / hgweb
  6. reduced dependencies on theory List_Permutation — haftmann / hgweb

#38 (Mar 7, 2021, 12:14:00 AM)

  1. obsolete (see f3378101f555); — wenzelm / hgweb
  2. merged — wenzelm / hgweb
  3. more direct unlimited smt_timeout;
    update of certificates: generated command-line options are part of input / digest; — wenzelm / hgweb
  4. clarified smt: support Timeout.ignored and Timeout.scale_time; — wenzelm / hgweb
  5. clarified timeouts in Isabelle/ML; — wenzelm / hgweb
  6. tuned --- more elementary Time operations; — wenzelm / hgweb
  7. removed unused/pointless operation: Time.start is the load/init time of this Scala module; — wenzelm / hgweb
  8. obsolete; — wenzelm / hgweb
  9. clarified signature --- augment existing structure Time; — wenzelm / hgweb
  10. rebuild SMT certificates from scratch; — wenzelm / hgweb
  11. added lemmas (sublist|prefix|suffix)_list_all — desharna / hgweb
  12. added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While — desharna / hgweb
  13. added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI — desharna / hgweb
  14. typo — haftmann / hgweb
  15. merged — desharna / hgweb
  16. added upper bound on monomorphisation duplicate instances — desharna / hgweb
  17. tuned best_slices in atp_config — desharna / hgweb
  18. tuned exec field in atp_config — desharna / hgweb
  19. removed junk; — wenzelm / hgweb
  20. tuned proofs; — wenzelm / hgweb
  21. enforce full build, after significant changes in Isabelle/Scala; — wenzelm / hgweb
  22. clarified compiler options: show relevant warnings; — wenzelm / hgweb
  23. tuned --- avoid compiler warnings; — wenzelm / hgweb
  24. clarified signature --- fewer warnings; — wenzelm / hgweb
  25. clarified signature --- fewer warnings; — wenzelm / hgweb
  26. tuned --- fewer warnings; — wenzelm / hgweb
  27. more robust ordering (see also 88c96e836ed6); — wenzelm / hgweb
  28. proper scala.collection.immutable; — wenzelm / hgweb
  29. tuned --- fewer warnings; — wenzelm / hgweb
  30. tuned --- fewer warnings; — wenzelm / hgweb
  31. tuned; — wenzelm / hgweb
  32. tuned --- fewer warnings; — wenzelm / hgweb
  33. tuned --- fewer warnings; — wenzelm / hgweb
  34. tuned --- fewer warnings; — wenzelm / hgweb
  35. tuned --- fewer warnings; — wenzelm / hgweb
  36. more robust error; — wenzelm / hgweb
  37. tuned --- fewer warnings; — wenzelm / hgweb
  38. tuned --- fewer warnings; — wenzelm / hgweb
  39. tuned --- fewer warnings; — wenzelm / hgweb
  40. updated to scala-2.13.5 (with scala-swing_2.13-3.0.0); — wenzelm / hgweb
  41. slightly more efficient Term.fastype_of (only little impact in regular applications); — wenzelm / hgweb
  42. reduced dependencies on theory List_Permutation — haftmann / hgweb
  43. Merge — paulson <lp15@cam.ac.uk> / hgweb
  44. reverted simprule status on a new lemma — paulson <lp15@cam.ac.uk> / hgweb
  45. merged — paulson / hgweb
  46. tiny bit of lemma hacking — paulson <lp15@cam.ac.uk> / hgweb
  47. tuned --- fewer warnings; — wenzelm / hgweb
  48. tuned --- fewer warnings; — wenzelm / hgweb
  49. tuned --- avoid deprecated conversions between certain number type; — wenzelm / hgweb
  50. tuned --- avoid deprecated Predef.any2stringadd; — wenzelm / hgweb
  51. tuned --- silence odd warning; — wenzelm / hgweb
  52. tuned --- fewer warnings; — wenzelm / hgweb
  53. tuned --- fewer warnings; — wenzelm / hgweb
  54. tuned --- fewer warnings; — wenzelm / hgweb
  55. tuned --- fewer warnings; — wenzelm / hgweb
  56. clarified signature, according to Isabelle/Scala; — wenzelm / hgweb
  57. download more directly, via means of JVM; — wenzelm / hgweb
  58. download on separate thread; — wenzelm / hgweb
  59. clarified signature; — wenzelm / hgweb
  60. tuned; — wenzelm / hgweb
  61. proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.); — wenzelm / hgweb
  62. tuned signature; — wenzelm / hgweb
  63. NEWS — haftmann / hgweb
  64. lemma diffusion — haftmann / hgweb
  65. more connections between mset _ = mset _ and permutations — haftmann / hgweb
  66. dissolve theory with duplicated name from afp — haftmann / hgweb
  67. more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept; — wenzelm / hgweb
  68. more Isabelle/ML/Scala operations; — wenzelm / hgweb
  69. more Isabelle/ML/Scala operations; — wenzelm / hgweb
  70. more Isabelle/ML/Scala operations;
    clarified errors; — wenzelm / hgweb
  71. proper src1, amending 20157c8ab3f3; — wenzelm / hgweb
  72. tuned; — wenzelm / hgweb
  73. proper File.eq, amending df49ca5da9d0; — wenzelm / hgweb
  74. tuned; — wenzelm / hgweb
  75. clarified modules: more like ML; — wenzelm / hgweb
  76. obsolete; — wenzelm / hgweb
  77. tuned; — wenzelm / hgweb
  78. more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552); — wenzelm / hgweb
  79. discontinued somewhat pointless "integrity test of build_history": it fails right now, but also failed to expose spurious incompatibilities when it was working; — wenzelm / hgweb

#38 (Mar 7, 2021, 12:14:00 AM)

  1. tuned — nipkow / hgweb
  2. Tuned presentation of Buffon's needle — Manuel Eberl <eberlm@in.tum.de> / hgweb
  3. tuned — nipkow / hgweb
  4. reduced dependencies on theory List_Permutation — haftmann / hgweb
  5. tidied up messy proofs — paulson <lp15@cam.ac.uk> / hgweb
  6. lemma diffusion — haftmann / hgweb
  7. more connections between mset _ = mset _ and permutations — haftmann / hgweb
  8. dissolve theory with duplicated name from afp — haftmann / hgweb

#37 (Feb 28, 2021, 12:14:00 AM)

  1. more checks; — wenzelm / hgweb
  2. clarified message; — wenzelm / hgweb
  3. clarified message; — wenzelm / hgweb
  4. clarified comments; — wenzelm / hgweb
  5. clarified message; — wenzelm / hgweb
  6. improved list_neq simproc — nipkow / hgweb
  7. merged — haftmann / hgweb
  8. repaired document — haftmann / hgweb
  9. merged — paulson / hgweb
  10. merged — paulson / hgweb
  11. A couple of basic lemmas about arg — paulson <lp15@cam.ac.uk> / hgweb
  12. multiset as equivalence class of permuted lists — haftmann / hgweb
  13. emphasize connection to multisets — haftmann / hgweb
  14. proper "latest" tag, otherwise the default pull command from https://hub.docker.com/r/makarius/isabelle won't work; — wenzelm / hgweb
  15. more on Isabelle_System.bash; — wenzelm / hgweb
  16. more specific name — haftmann / hgweb
  17. more lemmas — haftmann / hgweb
  18. dropped obscure FIXME — haftmann / hgweb
  19. proper usage of hypotheses for zipperposition's TPTP generation — desharna / hgweb
  20. merged — desharna / hgweb
  21. tuned Mirabelle to parse option check_trivial only once — desharna / hgweb
  22. merged — desharna / hgweb
  23. merged — desharna / hgweb
  24. added stride option to Mirabelle — desharna / hgweb
  25. proper prover capabilities for zipperposition — desharna / hgweb
  26. NEWS; — wenzelm / hgweb
  27. merged — wenzelm / hgweb
  28. clarified uses of Isabelle_System.bash_process: more checks, fewer messages; — wenzelm / hgweb
  29. tuned signature; — wenzelm / hgweb
  30. more direct timing from bash_process wrapper; — wenzelm / hgweb
  31. tuned; — wenzelm / hgweb
  32. clarified signature, following Isabelle/Scala; — wenzelm / hgweb
  33. tuned; — wenzelm / hgweb
  34. clarified signature; — wenzelm / hgweb
  35. clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code; — wenzelm / hgweb
  36. clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala; — wenzelm / hgweb
  37. tuned; — wenzelm / hgweb
  38. clarified signature, following Isabelle/Scala; — wenzelm / hgweb
  39. tuned signature; — wenzelm / hgweb
  40. clarified signature: process_result timing from Isabelle/Scala; — wenzelm / hgweb
  41. NEWS — haftmann / hgweb
  42. dedicated locale for preorder and abstract bdd operation — haftmann / hgweb
  43. get rid of traditional predicate — haftmann / hgweb
  44. proper treatment of process_result; — wenzelm / hgweb
  45. more accurate process_result in ML, corresponding to Process_Result in Scala; — wenzelm / hgweb
  46. clarified: proper trim_line for error; — wenzelm / hgweb
  47. unused; — wenzelm / hgweb
  48. clarified lines (again); — wenzelm / hgweb
  49. clarified modules; — wenzelm / hgweb
  50. more uniform Bash.process: always ask Isabelle/Scala; — wenzelm / hgweb
  51. more reactive protocol messages, e.g. for Scala.function (relevant for Bash.process); — wenzelm / hgweb
  52. clarified compiler options; — wenzelm / hgweb
  53. tuned comments; — wenzelm / hgweb
  54. removed obsolete RC tags; — wenzelm / hgweb

#37 (Feb 28, 2021, 12:14:00 AM)

  1. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  2. revert accidental change — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  3. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  4. website update — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  5. fix typo (Bauer -> Bayer) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  6. new entry BTree — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  7. add Windows example to use-instructions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  8. Isabelle app layout changed on Mac — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  9. Formal_Puiseux_Series website — paulson <lp15@cam.ac.uk> / hgweb
  10. new entry Formal_Puiseux_Series — paulson <lp15@cam.ac.uk> / hgweb
  11. 2021 web pages — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  12. update with 2021 release .tar.gz's — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  13. add Isabelle2021 release date — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  14. update .tar.gz releases — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  15. set version to 2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  16. multiset as equivalence class of permuted lists — haftmann / hgweb
  17. emphasize connection to multisets — haftmann / hgweb
  18. more specific name — haftmann / hgweb
  19. merged — wenzelm / hgweb
  20. adapted to Isabelle/0110e2e2964c; — wenzelm / hgweb
  21. adapted to Isabelle/f0db1e4c89bc; — wenzelm / hgweb
  22. dedicated locale for preorder and abstract bdd operation — haftmann / hgweb
  23. get rid of traditional predicate — haftmann / hgweb
  24. more accurate process_result; — wenzelm / hgweb
  25. adapted to Isabelle/440546ea20e6; — wenzelm / hgweb

#36 (Feb 21, 2021, 12:14:00 AM)

  1. more hints; — wenzelm / hgweb
  2. merged — wenzelm / hgweb
  3. Added tag Isabelle2021 for changeset 7e2a9a8c2b85 — wenzelm / hgweb
  4. provide naproche-755224402e36; — wenzelm / hgweb
  5. provide naproche-4ad61140062f; — wenzelm / hgweb
  6. HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc. — Manuel Eberl <eberlm@in.tum.de> / hgweb
  7. tidied up a few ugly proofs — paulson <lp15@cam.ac.uk> / hgweb
  8. merged — wenzelm / hgweb
  9. provide naproche-6d0d76ce2f2a; — wenzelm / hgweb
  10. Added tag Isabelle2021-RC6 for changeset ed36e33a2e4b — wenzelm / hgweb
  11. updated to flatlaf-1.0; — wenzelm / hgweb
  12. tuned NEWS; — wenzelm / hgweb
  13. tuned comments; — wenzelm / hgweb
  14. more robust interrupt handling as in Future.forked_results (amending 64df1e514005); — wenzelm / hgweb
  15. more parallelism: avoid exhaustion of standard thread pool; — wenzelm / hgweb

#36 (Feb 21, 2021, 12:14:00 AM)

  1. follow_on changes from Complex_Geometry — paulson <lp15@cam.ac.uk> / hgweb
  2. merged — paulson / hgweb
  3. a massive simplification, thanks to sledgehammer, etc. — paulson <lp15@cam.ac.uk> / hgweb
  4. adapted to isabelle-dev/73253:f6bb31879698 — Manuel Eberl <eberlm@in.tum.de> / hgweb
  5. Buffons_Needle: tuned presentation — Manuel Eberl <eberlm@in.tum.de> / hgweb
  6. Ergodic_Theory: removed 'pullback_algebra'. Turns out it already exists and is called 'vimage_algebra'. — Manuel Eberl <eberlm@in.tum.de> / hgweb

#34 (Feb 7, 2021, 12:14:00 AM)

  1. merged — wenzelm / hgweb
  2. updated for release; — wenzelm / hgweb
  3. Added tag Isabelle2021-RC4 for changeset 2ab14dbc6feb — wenzelm / hgweb
  4. provide naproche-20210201; — wenzelm / hgweb
  5. clarified messages; — wenzelm / hgweb
  6. more parallel; — wenzelm / hgweb
  7. more parallel; — wenzelm / hgweb
  8. contributors — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  9. hide the internal abbreviations MR and MB — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  10. optimize RBT_Impl — mraszyk / hgweb
  11. merged — wenzelm / hgweb
  12. more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup); — wenzelm / hgweb
  13. tuned signature: more types; — wenzelm / hgweb
  14. clarified signature: proper order; — wenzelm / hgweb
  15. clarified signature: more explicit types; — wenzelm / hgweb
  16. tuned; — wenzelm / hgweb
  17. clarified signature: no symbol markup within XML attributes; — wenzelm / hgweb
  18. clarified signature; — wenzelm / hgweb
  19. tuned signature; — wenzelm / hgweb
  20. bundle more libraries from scala-2.12.x, notably for Isabelle/MMT; — wenzelm / hgweb
  21. provide naproche-20210129; — wenzelm / hgweb
  22. more robust type signatures, notably for the sake of haskell-stack-trace-plugin-0.1.1.1; — wenzelm / hgweb
  23. tuned signature (e.g. see HTML.control_block in Isabelle/Scala); — wenzelm / hgweb
  24. proper Isabelle environment (amending 31fbde3baa97); — wenzelm / hgweb
  25. updated to jdk-15.0.2+7; — wenzelm / hgweb
  26. follow Phabricator update 2021 Week 4; — wenzelm / hgweb
  27. more NEWS; — wenzelm / hgweb
  28. more uniform directory layout for macOS;
    uniform Isabelle_app executable + lib/scripts/Isabelle_app for Linux and macOS;
    proper support for Apple "Files and Folders" security via x86_64-darwin executable (which is still able to launch arm64-darwin Java); — wenzelm / hgweb
  29. more generic Isabelle_app; — wenzelm / hgweb
  30. prefer dynamic linking: platform is always x86_64 (see 373dcdd363dc); — wenzelm / hgweb
  31. more robust; — wenzelm / hgweb
  32. tuned; — wenzelm / hgweb
  33. tuned; — wenzelm / hgweb
  34. provide jdk-11.0.10+9.tar.gz LTS for testing (inactive); — wenzelm / hgweb

#34 (Feb 7, 2021, 12:14:00 AM)

  1. merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  2. merge from afp-2020 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
  3. fixed category for Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
  4. Backed out changeset 4450302adc70 — Manuel Eberl <eberlm@in.tum.de> / hgweb
  5. fixed category for Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
  6. sitegen for Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
  7. New entry: Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
  8. paragraph tags in the abstract of IsaGeoCoq — paulson <lp15@cam.ac.uk> / hgweb
  9. tidying of IsaGeoCoq including a shorter abstract and revised title — paulson <lp15@cam.ac.uk> / hgweb
  10. website for IsaGeoCoq — paulson <lp15@cam.ac.uk> / hgweb
  11. new entry IsaGeoCoq — paulson <lp15@cam.ac.uk> / hgweb
  12. hide MB abbreviation — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
  13. integrate RBT_Impl optimizations — mraszyk / hgweb

#33 (Jan 31, 2021, 12:14:00 AM)

  1. Simpler proof — nipkow / hgweb
  2. more robust: support other_isabelle.init_settings for build_history before b93404a4c3dd; — wenzelm / hgweb
  3. more robust: defer error in sessions structure to build process; — wenzelm / hgweb
  4. merged, with minor edits: Admin/PLATFORMS, CONTRIBUTORS; — wenzelm / hgweb
  5. Added tag Isabelle2021-RC3 for changeset 02422c9add5e — wenzelm / hgweb
  6. provide naproche-20210124 (inactive); — wenzelm / hgweb
  7. follow stackage update; — wenzelm / hgweb
  8. tuned name, e.g. relevant for Naproche-SAD debugging in Isabelle/jEdit; — wenzelm / hgweb
  9. more operations for client connection; — wenzelm / hgweb
  10. fewer warnings, notably in Naproche-SAD; — wenzelm / hgweb
  11. suppress bundled Naproche-SAD component: it is in conflict with building the same from sources; — wenzelm / hgweb
  12. more robust etc/settings; — wenzelm / hgweb
  13. IDE support for Naproche-SAD; — wenzelm / hgweb
  14. proper path; — wenzelm / hgweb
  15. support isabelle components -u and -x; — wenzelm / hgweb
  16. proper typescript version, required for "vsce package"; — wenzelm / hgweb
  17. auto-update; — wenzelm / hgweb
  18. auto-update; — wenzelm / hgweb
  19. proper type constraint; — wenzelm / hgweb
  20. VSCode extension for official Isabelle release; — wenzelm / hgweb
  21. proper message; — wenzelm / hgweb
  22. unused; — wenzelm / hgweb
  23. proper heap_free; — wenzelm / hgweb
  24. suppress markup for literal tokens with block control symbols, for better PIDE/HTML output (see also d15fe10593ff); — wenzelm / hgweb
  25. clarified documentation concerning macOS Big Sur; — wenzelm / hgweb
  26. more systematic java-gui-setup, also for "isabelle jedit" command-line tool; — wenzelm / hgweb
  27. updated to flatlaf-1.0-rc1; — wenzelm / hgweb
  28. tuned; — wenzelm / hgweb
  29. tuned proofs; — wenzelm / hgweb
  30. tuned; — wenzelm / hgweb
  31. obsolete; — wenzelm / hgweb
  32. clarified platforms; — wenzelm / hgweb
  33. more NEWS; — wenzelm / hgweb
  34. workaround for Big Sur fullscreen mode: better support for JDialog windows (e.g. Find on top of main View); — wenzelm / hgweb
  35. clarified app identification, potentially relevant for macOS "defaults"; — wenzelm / hgweb
  36. updated documentation: HIDPI works smoothly thanks to FlatLaf; — wenzelm / hgweb
  37. updated for release; — wenzelm / hgweb
  38. updated screenshot; — wenzelm / hgweb
  39. clarified reports before errors: support completion of bibtex entries in Isabelle/Scala (amending d01ea9e3bd2d); — wenzelm / hgweb
  40. tuned; — wenzelm / hgweb
  41. proper theory_long_name; — wenzelm / hgweb
  42. updated screenshots; — wenzelm / hgweb
  43. more robust GUI, notably for Big Sur full-screen where the hypersearch panel becomes a separate maximized window; — wenzelm / hgweb
  44. revert 1105c42722dc on isabelle-release branch; — wenzelm / hgweb

#33 (Jan 31, 2021, 12:14:00 AM)

  1. Merge — Simon Foster <simon.foster@york.ac.uk> / hgweb
  2. Small update to Optics document. — Simon Foster <simon.foster@york.ac.uk> / hgweb
  3. merged — wenzelm / hgweb
  4. more generous timeout (25min CPU time); — wenzelm / hgweb
  5. non-executable files; — wenzelm / hgweb
  6. Added metadata for previous commit (Optics). — Simon Foster <simon.foster@york.ac.uk> / hgweb
  7. Addition of theorems throughout, particularly for prisms.
    New "chantype" command allows the definition of an algebraic datatype with generated prisms.
    New "dataspace" command allows the definition of a local-based state space, including lenses and prisms.
    Addition of various examples. — Simon Foster <simon.foster@york.ac.uk> / hgweb
  8. adjustments for Word_Lib updates — kleing / hgweb
  9. sync with l4v — kleing / hgweb
  10. allow instance for nat

    (by Florian) — kleing / hgweb
  11. merge from afp-2020 — kleing / hgweb
  12. New entry JinjaDCI — nipkow / hgweb

#31 (Jan 17, 2021, 12:14:00 AM)

  1. back to post-release mode; — wenzelm / hgweb
  2. Added tag Isabelle2021-RC2 for changeset 802647edfe7b — wenzelm / hgweb
  3. tuned; — wenzelm / hgweb
  4. avoid Unicode quotes; — wenzelm / hgweb
  5. clarified pretty margin: attempt to avoid scrollbar; — wenzelm / hgweb
  6. more documentation; — wenzelm / hgweb
  7. more informative errors: simplify diagnosis of spurious failures reported by users; — wenzelm / hgweb