Changes
#96 (Mar 20, 2022, 12:14:00 AM)
- Tidied several ugly proofs in some elderly examples — paulson <lp15@cam.ac.uk> / hgweb
- tuned message; — wenzelm / hgweb
- clarified errors; — wenzelm / hgweb
- tuned messages; — wenzelm / hgweb
- support Node.js as well, reusing the engine from Electron/VSCodium; — wenzelm / hgweb
- updated to vscode 1.65.2; — wenzelm / hgweb
- proper result check; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified directory layout and settings: more robust on all platforms; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- support Electron application framework;
clarified vscodium startup; — wenzelm / hgweb - generated lemma map_ident_strong for BNFs — desharna / hgweb
- updated SMT certificates — desharna / hgweb
- used more descriptive assert names in SMT-Lib output — desharna / hgweb
#95 (Mar 13, 2022, 12:14:00 AM)
- clarified and unified executable names; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- merged — wenzelm / hgweb
- suppress OCaml icons: avoid conflict of .ml and .ML, due to case-insensitive file-names in VSCode; — wenzelm / hgweb
- fix handling of lambdas in reconstruction of eq_congruent — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
- more robust: avoid breakdown of Search dialog; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- always use Isabelle encoding, as in Isabelle/jEdit; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified signature: more uniform ts vs. Scala; — wenzelm / hgweb
- discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249;
discontinued special treatment of workspace_dir as session directory; — wenzelm / hgweb - actually decode/encode symbols; — wenzelm / hgweb
- merged — wenzelm / hgweb
- prefer yarn over npm; — wenzelm / hgweb
- more accurate .hgignore; — wenzelm / hgweb
- clarified startup of "isabelle vscode": vscodium component is required, with patches for Isabelle/VSCode; — wenzelm / hgweb
- tuned messages; — wenzelm / hgweb
- proper init_resources for macos; — wenzelm / hgweb
- clarified names; — wenzelm / hgweb
- clarified modules: vscode vs. extension;
clarified signature; — wenzelm / hgweb - inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs; — wenzelm / hgweb
- more operations; — wenzelm / hgweb
- tuned comments;
tuned messages; — wenzelm / hgweb - patch VSCode source tree to support isabelle_encoding.ts; — wenzelm / hgweb
- more robust, pass "yarn valid-layers-check"; — wenzelm / hgweb
- clarified directories; — wenzelm / hgweb
- patch for vscode encoding "UTF-8-Isabelle": clone of "utf8", no symbols yet; — wenzelm / hgweb
- fit into vscode source conventions; — wenzelm / hgweb
- A tiny further cleanup — paulson <lp15@cam.ac.uk> / hgweb
- Tidied some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
- merged — nipkow / hgweb
- more count_list lemmas — nipkow / hgweb
- towards UTF-8-Isabelle symbol encoding; — wenzelm / hgweb
- updated to VSCode 1.65.0; — wenzelm / hgweb
- clarified char symbols: cover most European languages; — wenzelm / hgweb
- more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML); — wenzelm / hgweb
- tuned comments;
tuned imports; — wenzelm / hgweb - more robust dependencies: avoid implicit update, escpecially of underlying vscode engine; — wenzelm / hgweb
- proper file headers; — wenzelm / hgweb
- added count_list lemmas — nipkow / hgweb
- tuned message; — wenzelm / hgweb
- more compact result; — wenzelm / hgweb
- prepare patched version more thoroughly, with explicit patches; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
#95 (Mar 13, 2022, 12:14:00 AM)
- more count_list lemmas — nipkow / hgweb
- more count_list — nipkow / hgweb
- merged — nipkow / hgweb
- moved some count_list lemmas — nipkow / hgweb
- synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
- synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
- synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
- synchronize with https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/tree/5f38d029bfcabac8ba3b4ceea747f07772d1390d — Frédéric Tuong / hgweb
- continue 98838b260ed4 — Frédéric Tuong / hgweb
- continue ee01bce2ecca — Frédéric Tuong / hgweb
- cancel some part of 11d4567f1b99 — Frédéric Tuong / hgweb
- cancel some part of 98838b260ed4 — Frédéric Tuong / hgweb
- cancel some part of ada85c62541d — Frédéric Tuong / hgweb
- 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)
- recover platform-specific node binaries from original download, notably for node-pty for Terminal; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned imports; — wenzelm / hgweb
- misc tuning and clarification; — wenzelm / hgweb
- more executable files;
clarified modules; — wenzelm / hgweb - tuned; — wenzelm / hgweb
- tuned output; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified command-line options; — wenzelm / hgweb
- update official Isabelle release, notably for "Admin/init -R"; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- build component for VSCodium (cross-compiled from sources for all platforms); — wenzelm / hgweb
- tuned signature: more robust operation; — wenzelm / hgweb
- clarified order; — wenzelm / hgweb
- proper antiquotations (amending ff784d5a5bfb); — wenzelm / hgweb
- clarified signature: file operations take standard_path as in Isabelle/ML/Scala; — wenzelm / hgweb
- provide symbols statically via ISABELLE_VSCODE_WORKSPACE, instead of LSP/PIDE protocol; — wenzelm / hgweb
- proper init of non-existing file; — wenzelm / hgweb
- proper function call; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified modules: more uniform .scala vs. ts (amending 4519eeefe3b5); — wenzelm / hgweb
- misc tuning, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified signature;
clarified data structures; — wenzelm / hgweb - tuned imports; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- misc tuning, based on suggestions by IntelliJ IDEA; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- support for file-system operations; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- follow standard Isabelle license --- no longer published on market place; — wenzelm / hgweb
- tuned README; — wenzelm / hgweb
- disregard public marketplace; — wenzelm / hgweb
- tuned imports; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- merged — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- clarified module; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- added documentation for new VSCode modules; — Fabian Huch <huch@in.tum.de> / hgweb
- proper monospace font for terminal; — wenzelm / hgweb
- merged — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- support system path representations (as in Isabelle/Java/Scala); — wenzelm / hgweb
- auto-update; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified rendering; — wenzelm / hgweb
- prefer hardwired locale; — wenzelm / hgweb
- more aggressive activation; — wenzelm / hgweb
- Added some theorems (from Wetzel) — paulson <lp15@cam.ac.uk> / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- disable extension updates; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- disable check for updates: support just one static version; — wenzelm / hgweb
- misc tuning based on comments by Heiko Eißfeldt; — wenzelm / hgweb
- misc tuning based on comments by Heiko Eißfeldt; — wenzelm / hgweb
#94 (Mar 6, 2022, 12:14:00 AM)
- split locale in two — desharna / hgweb
- Stronger strong completeness result and variant that uses variables as Henkin witnesses. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Stronger strong completeness result and variant that uses variables as Henkin witnesses. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- added some alternative proofs in Smith_Normal_Form entry — jodivaso / hgweb
- The last tranche of material to be moved to the complex analysis libraries — paulson <lp15@cam.ac.uk> / hgweb
- 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)
- removed junk; — wenzelm / hgweb
- some updates to README.md; — wenzelm / hgweb
- clarified default settings; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- support Isabelle fonts via patch of vscode resources; — wenzelm / hgweb
- proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249); — wenzelm / hgweb
- clarified symbolic path; — wenzelm / hgweb
- clarified extension name (again); — wenzelm / hgweb
- removed obsolete material; — wenzelm / hgweb
- update scripts, based on recent "yo code" template; — wenzelm / hgweb
- clarified extension name (again), corresponding to qualified resources within VSCode (settings, commands, etc.); — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified extension name; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified options; — wenzelm / hgweb
- support local .vsix installation;
discontinued publishing to VSCode Marketplace, which will become obsolete eventually; — wenzelm / hgweb - formal record of generated package-lock.json; — wenzelm / hgweb
- pro-forma update of version, for ongoing development; — wenzelm / hgweb
- updated notes on Isabelle/VSCode development; — wenzelm / hgweb
- proper engines.vscode (amending c04ccea8bdd2): required for "vsce package", e.g. via "isabelle build_vscode; — wenzelm / hgweb
- simp rules for negative numerals — haftmann / hgweb
- updated vscode extension: proper recoding; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned vscode extension; — Fabian Huch <huch@in.tum.de> / hgweb
- tuned vscode extension: split isabelle fsp into workspace and mapping; — Fabian Huch <huch@in.tum.de> / hgweb
- update VSCode plugin dependencies; — Fabian Huch <huch@in.tum.de> / hgweb
- added Isabelle output panel to VSCode extension; — Fabian Huch <huch@in.tum.de> / hgweb
- Simplified a couple of extremely long and ugly apply-proofs — paulson <lp15@cam.ac.uk> / hgweb
- merged — wenzelm / hgweb
- some updates to README.md; — wenzelm / hgweb
- refer to Isabelle settings via environment, which is provided via "isabelle vscode";
clarified error handling; — wenzelm / hgweb - more operations; — wenzelm / hgweb
- more robust startup wrt. VSCode workspace (by Fabian Huch); — wenzelm / hgweb
- various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch); — wenzelm / hgweb
- have Sledgehammer honor 'smt_nat_as_int' option — blanchet / hgweb
- more handling of Zipperposition definitions in Isar proof construction — blanchet / hgweb
- handle Zipperposition definitions in Isar proof construction — blanchet / hgweb
- parse Zipperposition definitions — blanchet / hgweb
- clarified URL; — wenzelm / hgweb
- clarified pdf path; — wenzelm / hgweb
- HTTP view of Isabelle PDF documentation; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- clarified signature: more explicit section structure; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified URL (again); — wenzelm / hgweb
- more robust toplevel url: allow extra "/"; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature;
clarified URLs; — wenzelm / hgweb - clarified signature; — wenzelm / hgweb
- support for PDF.js: platform-independent PDF viewer; — wenzelm / hgweb
- more robust mime_type; — wenzelm / hgweb
- merged — wenzelm / hgweb
- 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
- one new lemma — paulson <lp15@cam.ac.uk> / hgweb
- clarified options; — wenzelm / hgweb
- clarified options; — wenzelm / hgweb
- clarified directory; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- prefer strict equality, without implicit type conversion; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- auto-update by VSCode; — wenzelm / hgweb
- more activationEvents, as proposed by Denis Paluca; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- NEWS; — wenzelm / hgweb
- run Isabelle/VSCode using local VSCodium installation; — wenzelm / hgweb
- provide macos_exe, based on bin/codium from linux; — wenzelm / hgweb
- clarified options; — wenzelm / hgweb
- Avoid overaggresive splitting. — haftmann / hgweb
- more lemmas for distribution — haftmann / hgweb
- Avoid overaggresive simplification. — haftmann / hgweb
- merged — wenzelm / hgweb
- setup VSCode from VSCodium distribution; — wenzelm / hgweb
- more robust package_dir, to increase chances that it works with IntelliJ IDEA; — wenzelm / hgweb
- NEWS — desharna / hgweb
- Mirabelle now considers goals preceding "unfolding" and "using" commands — desharna / hgweb
#93 (Feb 27, 2022, 12:14:00 AM)
- Deleted nearly 200 lines of unused material — paulson <lp15@cam.ac.uk> / hgweb
- A new theorem — paulson <lp15@cam.ac.uk> / hgweb
- Clarified code module names. — haftmann / hgweb
- removed ancient numeral representation — haftmann / hgweb
- restore state of VYDRA_MDL to b8c3f69745a4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- metadata for Universal_Hash_Families — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Universal_Hash_Families — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- New entry Wetzel's Problem — nipkow / hgweb
- metadata for Eval_FO — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Eval_FO — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata for VYDRA_MDL — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry VYDRA_MDL — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- Backed out changeset c9f94b0ae10e — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Backed out changeset b8c3f69745a4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- metadata update for VYDRA_MDL — mraszyk / hgweb
- New entry: VYDRA_MDL — mraszyk / hgweb
- fixed failing proofs — desharna / hgweb
- New definition of the Aleph operator so that it's defined for all arguments, not just ordinals — paulson <lp15@cam.ac.uk> / hgweb
- ALEXANDRIA acknowledgements — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- New set theory lemmas about cardinality (mainly) — paulson <lp15@cam.ac.uk> / hgweb
- Another attempt for a consolidated terminology. — haftmann / hgweb
- Avoid overaggresive splitting. — haftmann / hgweb
- more lemmas for distribution — haftmann / hgweb
- Avoid overaggresive simplification. — haftmann / hgweb
- some new lemmas — paulson <lp15@cam.ac.uk> / hgweb
#92 (Feb 20, 2022, 12:14:00 AM)
- merged — paulson / hgweb
- an assortment of new or stronger lemmas — paulson <lp15@cam.ac.uk> / hgweb
- obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented; — wenzelm / hgweb
- print outcome of Sledgehammer search in panel — blanchet / hgweb
- print Sledgehammer error message — blanchet / hgweb
#92 (Feb 20, 2022, 12:14:00 AM)
- merged — nipkow / hgweb
- More material — nipkow / hgweb
- added idempotent most general unifier — desharna / hgweb
- used same parameter order for locales substitution and substitution — desharna / hgweb
- patched for new/simplified lemmas — paulson <lp15@cam.ac.uk> / hgweb
- Better notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
#91 (Feb 13, 2022, 12:14:00 AM)
- updated documentation to current matter of affairs — haftmann / hgweb
- unused; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- merged — desharna / hgweb
- added Isabelle identification to Mirabelle output — desharna / hgweb
- uniformized fact selection for ATP and SMT in Sledgehammer — desharna / hgweb
- provide cache for slow computations; — wenzelm / hgweb
- used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer — desharna / hgweb
- more operations; — wenzelm / hgweb
- more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson) — blanchet / hgweb
- more robust TSTP proof parsing — blanchet / hgweb
- added possibility of extra options to SMT slices — blanchet / hgweb
#91 (Feb 13, 2022, 12:14:00 AM)
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- avoid conflict with index.html in generated html — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- New entry: FO_Theory_Rewriting — nipkow / hgweb
- Improve consistency of type-variables in WOOT_Strong_Eventual_Consistency.
+ Remove obsolete e-mail from notification mailing list. — Emin Karayel <me@eminkarayel.de> / hgweb - Improve proofs for Interpolation_Polynomials_HOL_Algebra.
Reduced the number of apply scripts used. — Emin Karayel <me@eminkarayel.de> / hgweb - Correct date. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- deleted a lemma that's in the devel library — paulson <lp15@cam.ac.uk> / hgweb
- Cleanup and new results. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- moved theorems into Matrix.thy — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge of AFP 2021-1 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- New AFP entry: Equivalence_Relation_Enumeration — nipkow / hgweb
- new entry: LP_Duality — nipkow / hgweb
- cosmetic tweaks — paulson <lp15@cam.ac.uk> / hgweb
- sitegen and metadata for Young's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Young's inequality — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata for Quasi_Borel_Spaces, sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Quasi_Borel_Spaces — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for FOL_Seq_Calc2 — paulson <lp15@cam.ac.uk> / hgweb
- new entry FOL_Seq_Calc2 — paulson <lp15@cam.ac.uk> / hgweb
- tweak: corollary that the ln also yields irrational numbers — paulson <lp15@cam.ac.uk> / hgweb
- New entry: Interpolation_Polynomials_HOL_Algebra — nipkow / hgweb
- Finally remembered to run sitegen — paulson <lp15@cam.ac.uk> / hgweb
- Fixed the meta data in the abstract as well — paulson <lp15@cam.ac.uk> / hgweb
- Eliminated the references to SOS (which is no longer used) and changed to the document style to "article". — paulson <lp15@cam.ac.uk> / hgweb
- typo — nipkow / hgweb
- typo — nipkow / hgweb
- New entry Irrationals_From_THEBOOK — nipkow / hgweb
- new entry Median_Method — nipkow / hgweb
- Actuarial Mathematics website — paulson <lp15@cam.ac.uk> / hgweb
- New entry Actuarial_Mathematics — paulson <lp15@cam.ac.uk> / hgweb
#90 (Feb 6, 2022, 12:14:00 AM)
- tuned output syntax: Hoare triples are now blocks — nipkow / hgweb
- tuned output syntax: INV and VAR are now blocks — nipkow / hgweb
- more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)') — blanchet / hgweb
- enable induction in one of Zipperposition's slices — blanchet / hgweb
- made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme — blanchet / hgweb
- robustly handle empty proof blocks in Isar proof output — blanchet / hgweb
- propagate right result when enough proofs have been found — blanchet / hgweb
- correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives — blanchet / hgweb
- don't lose error messages — blanchet / hgweb
- don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice — blanchet / hgweb
- careful with partial applications — blanchet / hgweb
- don't perform preplaying steps if preplaying is disabled — blanchet / hgweb
- adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs — blanchet / hgweb
- tuned punctuation — blanchet / hgweb
- handle TPTP '!=' more gracefully in Isar proof reconstruction — blanchet / hgweb
- guard against duplicate lines in Zipperposition proofs — blanchet / hgweb
- tuning — blanchet / hgweb
- tuned NEWS — blanchet / hgweb
- compile HOL-TPTP — blanchet / hgweb
- compile Metis_Examples — blanchet / hgweb
- more NEWS — blanchet / hgweb
- compile mirabelle — blanchet / hgweb
- tweaked Auto Sledgehammer's behavior and output — blanchet / hgweb
- updated NEWS — blanchet / hgweb
- removed experimental prover z3_tptp — blanchet / hgweb
- print more verbose information — blanchet / hgweb
- run all installed provers by default — blanchet / hgweb
- update slice options centrally — blanchet / hgweb
- further work on new Sledgehammer slicing — blanchet / hgweb
- tweaked verbose output — blanchet / hgweb
- tweak padding of prover slice schedule to include all provers — blanchet / hgweb
- implemented 'max_proofs' mechanism — blanchet / hgweb
- document new option 'max_proofs' — blanchet / hgweb
- crude implementation of centralized slicing — blanchet / hgweb
- removed obscure E option — blanchet / hgweb
- take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set — blanchet / hgweb
- rationalize slicing format — blanchet / hgweb
- thread slices through — blanchet / hgweb
- simplified 'best_slice' data structure and made minor changes to slices — blanchet / hgweb
- changed logic of 'slice' option to 'slices' — blanchet / hgweb
- updated documentation of 'slice' (now 'slices') option — blanchet / hgweb
- revised Sledgehammer documentation — blanchet / hgweb
- rationalized output for forthcoming slicing model — blanchet / hgweb
- use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code — blanchet / hgweb
- disable slicing within ATP module (in preparation for refactoring) — blanchet / hgweb
- disable slicing within SMT (in preparation for factoring it out) — blanchet / hgweb
- generalized the 'slice' option towards more flexible slicing — blanchet / hgweb
- tuned -- fewer warnings; — wenzelm / hgweb
#90 (Feb 6, 2022, 12:14:00 AM)
- Strong soundness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Strong soundness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Fix LaTeX issue. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Qualification required(?) — nipkow / hgweb
- merged — nipkow / hgweb
- more variants of the algorithm — nipkow / hgweb
- Added funding acknowledgments.
Fixed broken BibTeX citation. — Dominique Unruh <unruh@ut.ee> / hgweb - Strong completeness for PAL systems. — Asta Halkjær From <andro.from@gmail.com> / hgweb
#89 (Jan 30, 2022, 12:14:00 AM)
- Added a tiny proof — paulson <lp15@cam.ac.uk> / hgweb
- Deletion of a duplicate proof — paulson <lp15@cam.ac.uk> / hgweb
- useful lemma integral_less — paulson <lp15@cam.ac.uk> / hgweb
- merged — desharna / hgweb
- removed unused parameter following f9908452b282 — desharna / hgweb
- treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis) — blanchet / hgweb
- fixed dodgy intro! attributes — paulson <lp15@cam.ac.uk> / hgweb
- merged — desharna / hgweb
- optimized facts traversal in TPTP translation — desharna / hgweb
- optimized app_op_level selection in TPTP generation — desharna / hgweb
- tuned trivial check in mirabelle_sledgehammer — desharna / hgweb
- renamed run_action to run in Mirabelle.action record — desharna / hgweb
- added spying of fact filtering timing — desharna / hgweb
- tuned mirabelle_sledgehammer output — desharna / hgweb
- added spying to Sledgehammer — desharna / hgweb
- proper fact filter for dummy ATPs — desharna / hgweb
- added syping of fact filtering time to sledgehammer — desharna / hgweb
- removed unsynchronized references in mirabelle_sledgehammer — desharna / hgweb
- tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run — desharna / hgweb
- updated to polyml-test-15c840d48c9a; — wenzelm / hgweb
#89 (Jan 30, 2022, 12:14:00 AM)
- Cleanup. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Fewer parentheses around turnstile + remove unused lemmas. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Simplify proof of truth lemma. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Notation for `imply` and fewer parenthesis around turnstiles. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Abstract results to shorten proofs. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Better notation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merged — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- more symbols; — wenzelm / hgweb
- profer bundle lattice_syntax; — wenzelm / hgweb
- prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation' as intended; — wenzelm / hgweb
- 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
- avoid hardwired document output; — wenzelm / hgweb
- merged — paulson / hgweb
- deleting the overloading of div and mod, with its attendant ambiguities — paulson <lp15@cam.ac.uk> / hgweb
- 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)
- some updates and clarification on Assumption.export_term; — wenzelm / hgweb
- new theorem has_integral_UN — paulson <lp15@cam.ac.uk> / hgweb
- updated to jdk-17.0.2+8; — wenzelm / hgweb
- used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads — desharna / hgweb
- NEWS — desharna / hgweb
- added Mirabelle option "-y" for dry run — desharna / hgweb
- tuned garbage optimization — desharna / hgweb
- added cpu time (in ms) to Mirabelle run_action output — desharna / hgweb
- added Mirabelle option -r to randomize the goals before selection — desharna / hgweb
- A new lemma about inverse image — paulson <lp15@cam.ac.uk> / hgweb
- proper treatment of $let variables in symbol table in Sledgehammer — desharna / hgweb
- removed unconditional TPTP symbol declaration for undefined_bool in sledgehammer — desharna / hgweb
#88 (Jan 23, 2022, 12:14:00 AM)
- 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)
- merged — desharna / hgweb
- split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir" — desharna / hgweb
- proper name mangling of "undefined" constants in Sledgehammer — desharna / hgweb
- earlier availability of lifting — haftmann / hgweb
- more correct transfer — haftmann / hgweb
- merged — desharna / hgweb
- proper abstraction of function variables when instantiating induction rules in Sledgehammer — desharna / hgweb
- added lemma asympD — desharna / hgweb
- added lemma — nipkow / hgweb
- Some lemmas about continuous functions with integral zero — paulson <lp15@cam.ac.uk> / hgweb
#87 (Jan 16, 2022, 12:14:00 AM)
- Tuning. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- merged — paulson / hgweb
- tweaks — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Fixed an inadequate description — paulson <lp15@cam.ac.uk> / hgweb
- tuned — haftmann / hgweb
- mv to distribution — nipkow / hgweb
- by now in distribution — nipkow / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fixed abstract — nipkow / hgweb
- tuned — nipkow / hgweb
- website and metadata for Hyperdual — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Hyperdual — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sorted ROOTS — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- tuned — nipkow / hgweb
- New entry Knights_Tour — nipkow / hgweb
- more thoroughly replace Michael Foster's e-mail address — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata and sitegen for Gale_Shapley — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Gale_Shapley — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- update Michael Forster's email address — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata and sitegen for Roth_Arithmetic_Progressions — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Roth_Arithmetic_Progressions — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- typo — nipkow / hgweb
- merged — nipkow / hgweb
- New entry Regular_Tree_Relations — nipkow / hgweb
- We DON'T want an output directory — paulson <lp15@cam.ac.uk> / hgweb
- MDP-Algorithms website — paulson <lp15@cam.ac.uk> / hgweb
- new entry MDP-Algorithms — paulson <lp15@cam.ac.uk> / hgweb
- typo — paulson <lp15@cam.ac.uk> / hgweb
- new entry MDP-Rewards — paulson <lp15@cam.ac.uk> / hgweb
- fixed typo — paulson <lp15@cam.ac.uk> / hgweb
#86 (Jan 9, 2022, 12:14:00 AM)
- merged — desharna / hgweb
- added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp — desharna / hgweb
- removed $ite from E 2.6 in THF format — desharna / hgweb
- New and simplified theorems — paulson <lp15@cam.ac.uk> / hgweb
- merged — desharna / hgweb
- prefixed all mirabelle_sledgehammer output lines with sledgehammer output — desharna / hgweb
#86 (Jan 9, 2022, 12:14:00 AM)
- CS: possibility to disable backtracking; CZH: auxiliary results; ETTS: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
- used wfP_imp_asymp from HOL — desharna / hgweb
- simplified proof some more — desharna / hgweb
- simplified proof — desharna / hgweb
- 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)
- added lemma — nipkow / hgweb
- Tiny additions inspired by Roth development — paulson <lp15@cam.ac.uk> / hgweb
#85 (Jan 2, 2022, 12:14:00 AM)
- Tweaked some failing proofs — paulson <lp15@cam.ac.uk> / hgweb
#84 (Dec 26, 2021, 12:14:00 AM)
- allow general command transactions with presentation; — wenzelm / hgweb
- more operations; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- support Gradle as alternative to Maven (again); — wenzelm / hgweb
- tuned mirabelle command-line help message — desharna / hgweb
- updated Mirabelle documentation — desharna / hgweb
- proper documentation for induction_rules Sledgehammer option — desharna / hgweb
- NEWS — desharna / hgweb
- merged — desharna / hgweb
- used TH1 for Leo-III in sledgehammer — desharna / hgweb
- tuned run_sledgehammer and called it directly from Mirabelle — desharna / hgweb
- exported Sledgehammer.launch_prover and use it in Mirabelle — desharna / hgweb
- proper filtering inf induction rules in Mirabelle — desharna / hgweb
- added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle — desharna / hgweb
- tuned ATP to use is_widely_irrelevant_const — desharna / hgweb
- added support for initialization messages to Mirabelle — desharna / hgweb
#84 (Dec 26, 2021, 12:14:00 AM)
#83 (Dec 19, 2021, 12:14:00 AM)
- tuned comment — blanchet / hgweb
- support for JSON:API; — wenzelm / hgweb
- support for Flarum server; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- tuned imports; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- clarified author names; — wenzelm / hgweb
- clarified author names; — wenzelm / hgweb
- merged — wenzelm / hgweb
- more accurate names;
complete coverage of mail addresses; — wenzelm / hgweb - more standard author_info; — wenzelm / hgweb
- clarified author info and cluster nodes; — wenzelm / hgweb
- more data integrity: name vs. address; — wenzelm / hgweb
- clarified signature: more operations; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more data integrity: name vs. address; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- merged — desharna / hgweb
- tuned ATP to use fold_index — desharna / hgweb
- tuned sledgehammer to use map_index — desharna / hgweb
- merged — wenzelm / hgweb
- more data integrity: name vs. address; — wenzelm / hgweb
- misc tuning and clarification; — wenzelm / hgweb
- clarified name; — wenzelm / hgweb
- more mailing list content; — wenzelm / hgweb
- more mailing list content; — wenzelm / hgweb
- updated links; — wenzelm / hgweb
- 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
- tuned ATP to use map_index — desharna / hgweb
- removed obsolete RC tags; — wenzelm / hgweb
- proper path; — wenzelm / hgweb
- merged, resolving conflict in src/Doc/Implementation/Logic.thy; — wenzelm / hgweb
- Added tag Isabelle2021-1 for changeset c2a2be496f35 — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- proper ML types (amending 1aa92bc4d356); — wenzelm / hgweb
- proper types for Scala.Fun instances (amending 1aa92bc4d356); — wenzelm / hgweb
- proper syntax category; — wenzelm / hgweb
#83 (Dec 19, 2021, 12:14:00 AM)
- Strengthened a lemma — paulson <lp15@cam.ac.uk> / hgweb
- updated the definition of scheme — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add change history — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- updated 2021-1 release dates -> web — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- ignore generated files — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add 2021-1 release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- set devel version again — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Added tag Isabelle2021-1 for changeset 11f8b03a88ad — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjust usage version — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- set release version — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update release dates — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- The version without integer indexes — paulson <lp15@cam.ac.uk> / hgweb
- The version without integer indexes — paulson <lp15@cam.ac.uk> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry Foundation_of_geometry — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Modified all design locale parameters to be nats instead of ints. Fixed proofs as required. — cledmonds / hgweb
- adjust for Isabelle2021-1-RC5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry Simplicial_complexes_and_boolean_functions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Modified all design locale parameters to be nats instead of ints. Fixed proofs as required. — cledmonds / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjust to Isabelle2021-1-RC5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- metadata and sitegen for Hahn_Jordan_Decomposition — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- added Mathematics/Measure theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Hahn_Jordan_Decomposition — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- New entry: Van_Emde_Boas_Trees — nipkow / hgweb
- New entry: Van_Emde_Boas_Trees — nipkow / hgweb
- metadata and sitegen for SimplifiedOntologicalArgument — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: SimplifiedOntologicalArgument — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Tuned: use a star in witness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Rename H to S in maximal_exactly_one. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Get rid of the sat abbreviation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add missing spaces in semantics_tm. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- No space in front of object-logic forall. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Non-conflicting name for boolean denotation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Simpler Hintikka definition. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add syntactic abbreviation for constants. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add papers to metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- In the definition of regular pair, switched from strict to non-strict — paulson <lp15@cam.ac.uk> / hgweb
- A slightly stronger lemma allowing slightly simpler proofs — paulson <lp15@cam.ac.uk> / hgweb
#82 (Dec 12, 2021, 12:14:00 AM)
- provide component naproche-20211211; — wenzelm / hgweb
- merged — wenzelm / hgweb
- more Mailman archives; — wenzelm / hgweb
- more Mailman content; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned metis to use map_index — desharna / hgweb
- merged — desharna / hgweb
- fixed HOL-TPTP — desharna / hgweb
- tuned vars_of_iterm — desharna / hgweb
- fixed TPTP generation of multi-arity expressions — desharna / hgweb
- proper handling of Hilbert choice in TFX logics — desharna / hgweb
- proper tptp_builtins — desharna / hgweb
- reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle — desharna / hgweb
- proper proxy for Hilbert choice in TPTP output — desharna / hgweb
- proper polymorphism for TH1 format in Sledgehammer — desharna / hgweb
- refactored $ite and $let configuration and added dummy_thf_reduced prover — desharna / hgweb
- tuned TPTP file names generated by Sledgehammer — desharna / hgweb
- tuned SMT-Lib file names generated by Mirabelle — desharna / hgweb
- added support for higher-order SMT proof search in Sledgehammer — desharna / hgweb
- separated FOOL from $ite/$let in TPTP output — desharna / hgweb
- missing latex font — nipkow / hgweb
- Rewrite: added links to docu, made more prominent — nipkow / hgweb
- discontinued old-style {* verbatim *} tokens; — wenzelm / hgweb
- tuned proof; — wenzelm / hgweb
- isabelle update_cartouches; — wenzelm / hgweb
- more symbolic latex_output via XML (using YXML within text); — wenzelm / hgweb
- tuned signature: remove unused; — wenzelm / hgweb
- prefer symbolic Latex.environment (typeset in Isabelle/Scala); — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified corner cases of syntax; — wenzelm / hgweb
- clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2); — wenzelm / hgweb
- a slightly simpler proof — paulson <lp15@cam.ac.uk> / hgweb
#82 (Dec 12, 2021, 12:14:00 AM)
- merged — desharna / hgweb
- generalized standard formula redundancy out of standard redundancy — desharna / hgweb
- merged — wenzelm / hgweb
- discontinued Parse.text; — wenzelm / hgweb
- discontinued old-style {* verbatim *} tokens; — wenzelm / hgweb
- weakened locale assumptions: wfP implies asymp — desharna / hgweb
- Add papers to metadata. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- refactored Standard_Redundancy_Criterion to not use ordering type classes — desharna / hgweb
- isabelle update_cartouches; — wenzelm / hgweb
- removed obsolete "extend" operation; — wenzelm / hgweb
- more symbolic latex_output via XML (using YXML within text);
re-use existing Latex.output_markup; — wenzelm / hgweb - prefer symbolic Latex.environment (typeset in Isabelle/Scala); — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
#81 (Dec 5, 2021, 12:14:00 AM)
- provide component naproche-2d99afe5c349; — wenzelm / hgweb
- merged — wenzelm / hgweb
- Added tag Isabelle2021-1-RC5 for changeset 8baf2e8b16e2 — wenzelm / hgweb
- more documentation about Type/Const antiquotations; — wenzelm / hgweb
- more documentation about document build options; — wenzelm / hgweb
- address problems with launch4j and jdk-17 (see also 41d009462d3c, copy of 41d009462d3c); — wenzelm / hgweb
- tuned --- fewer IDE warnings; — wenzelm / hgweb
- 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
- added definitions multp{DM,HO} and corresponding lemmas — desharna / hgweb
- added wfP_less to wellorder and wfP_less_multiset — desharna / hgweb
- restored lemmas less_multiset{DM,HO} inadvertently changed by c256bba593f3 — desharna / hgweb
- merged — desharna / hgweb
- added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset — desharna / hgweb
- redefined less_multiset to be based on multp — desharna / hgweb
- added lemmas multp_code_eq_multp and multeqp_code_eq_reflclp_multp — desharna / hgweb
- added lemmas multp_cancel, multp_cancel_add_mset, and multp_cancel_max — desharna / hgweb
- added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp — desharna / hgweb
- added lemma wfP_multp — desharna / hgweb
- added lemma mono_multp — desharna / hgweb
- added Multiset.multp as predicate equivalent of Multiset.mult — desharna / hgweb
- address problems with launch4j and jdk-17 (see also 41d009462d3c); — wenzelm / hgweb
- more robust build on midrange hardware; — wenzelm / hgweb
- clarified tests: omit somewhat pointless (unstable) results; — wenzelm / hgweb
- proper fields for gnuplot (amending b614e3e4146a); — wenzelm / hgweb
- tuned output; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- merged — wenzelm / hgweb
- more robust build on midrange hardware (despite 67d6f1708ea4); — wenzelm / hgweb
- Added tag Isabelle2021-1-RC4 for changeset 2336356d4180 — wenzelm / hgweb
- updated to polyml-5.9; — wenzelm / hgweb
- NEWS on "isabelle mirabelle"; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified default for kodkod_scala;
NEWS for proper release; — wenzelm / hgweb - maintain option kodkod_scala within theory context, to allow local modification; — wenzelm / hgweb
- NEWS for proper release; — wenzelm / hgweb
- updated to flatlaf-1.6.4; — wenzelm / hgweb
- avoid broken links: auxiliary files are not yet supported; — wenzelm / hgweb
- option document_comment_latex supports e.g. Dagstuhl LIPIcs; — wenzelm / hgweb
- more explicit type Latex.Tags;
generate isabelletags.sty from Isabelle/Scala, including comment.sty setup; — wenzelm / hgweb - 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 - removed pointless 'text_cartouche' command: regular 'text' already supports cartouches; — wenzelm / hgweb
- example: alternative document headings, based on more general document output markup; — wenzelm / hgweb
- more general document output: enclosing markup is defined in user-space; — wenzelm / hgweb
- clarified modules (see c299abcf7081); — wenzelm / hgweb
- output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- tuned signature: more explicit types for presentation; — wenzelm / hgweb
- more robust support for Windows line-endings; — wenzelm / hgweb
- source positions for document markup commands, e.g. to retrieve PIDE markup in presentation; — wenzelm / hgweb
- more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory; — wenzelm / hgweb
- clarified system option standard values: avoid oddities like "isabelle build -o document_output" producing directories named "true"; — wenzelm / hgweb
- more symbolic latex_output via XML (using YXML within text); — wenzelm / hgweb
- proper enclose_name (amending e77c5bfca9aa); — wenzelm / hgweb
- Latex.Output.latex_heading depends on option document_heading_prefix, e.g. relevant for Dagstuhl LIPIcs which prefers unaliased \section etc.; — wenzelm / hgweb
- more symbolic latex_output via XML; — wenzelm / hgweb
- clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab); — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- updated to verit-2021.06.2-rmx; — wenzelm / hgweb
- clarified HTML_Context.theory_exports: prefer value-oriented parallelism; — wenzelm / hgweb
- generate problems with correct logic for veriT — fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
- more parallelism, at the cost of potential duplicates of make_thy; — wenzelm / hgweb
- afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a); — wenzelm / hgweb
- more interrupts; — wenzelm / hgweb
- present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826;
eliminated implicit state: these theories are globally unique; — wenzelm / hgweb - tuned; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- tuned (see also e0d1d9203275); — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- spelling; — wenzelm / hgweb
#81 (Dec 5, 2021, 12:14:00 AM)
- 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
- Tuned: use a star in witness. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merge from afp-2021-1 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjust for new tags in Isabelle2021-1-RC4 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb
- In the definition of regular pair, switched from strict to non-strict — paulson <lp15@cam.ac.uk> / hgweb
- Rename H to S in maximal_exactly_one. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Get rid of the sat abbreviation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add missing spaces in semantics_tm. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- No space in front of object-logic forall. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Non-conflicting name for boolean denotation. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Simpler Hintikka definition. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Add syntactic abbreviation for constants. — Asta Halkjær From <andro.from@gmail.com> / hgweb
- fixed lemma following Isabelle/c256bba593f3 — desharna / hgweb
- fix dangerous context management — Simon Wimmer <wimmers@in.tum.de> / hgweb
#80 (Nov 28, 2021, 12:14:00 AM)
- added asymp_{less,greater} to preorder and moved mult1_lessE out — desharna / hgweb
- renamed multp_code_iff and multeqp_code_iff — desharna / hgweb
- simplified mult_cancel_max and introduced orginal lemma as mult_cancel_max0 — desharna / hgweb
- renamed Multiset.multp and Multiset.multeqp — desharna / hgweb
#79 (Nov 21, 2021, 12:14:00 AM)
- added lemmas — nipkow / hgweb
- merged — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- removed redundant test (see also 86fac52c2795, a9fea3f11cc0); — wenzelm / hgweb
- just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow); — wenzelm / hgweb
- proper version; — wenzelm / hgweb
- back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in Padic_Ints (AFP/7a2522dce834); — wenzelm / hgweb
- less ambitious parallelism: more direct read/write saves overall heap space and GC time; — wenzelm / hgweb
- slightly faster XML output: avoid too much regrowing of StringBuilder; — wenzelm / hgweb
- updated NEWS: arm64-linux support is almost complete; — wenzelm / hgweb
- update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9; — wenzelm / hgweb
- more material for HOL-Analysis.Infinite_Sum — Manuel Eberl <manuel@pruvisto.org> / hgweb
- more symbolic latex_output via XML; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- updated to polyml-5.9-610a153b941d -- close to final; — wenzelm / hgweb
- tuned signature (again): latex_output is likely to depend on context; — wenzelm / hgweb
- more symbolic latex output;
discontinued Latex.output_text, which is in conflict with symbolic output; — wenzelm / hgweb - tuned signature; — wenzelm / hgweb
- symbolic latex_output via XML, interpreted in Isabelle/Scala; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature: more privacy; — wenzelm / hgweb
- tuned output --- less redundancy; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- clarified signature: Latex.Output as parameter to Document_Build.Engine;
tuned; — wenzelm / hgweb - proper detection of ARM platform variants; — wenzelm / hgweb
- back to post-release mode; — wenzelm / hgweb
- updated for release; — wenzelm / hgweb
- Added tag Isabelle2021-1-RC3 for changeset 2b212c8138a5 — wenzelm / hgweb
- merged — wenzelm / hgweb
- updated to polyml-5.9-cc80e2b43c38, which also contains ARM64 on darwin (unused by default); — wenzelm / hgweb
- clarified HTML_Context: more explicit directory structure; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified properties: avoid empty entry; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
#79 (Nov 21, 2021, 12:14:00 AM)
- A slightly stronger lemma allowing slightly simpler proofs — paulson <lp15@cam.ac.uk> / hgweb
- Complex_Bounded_Operators: Removed some lemmas from Extra_General that are now in Isabelle itself — Dominique Unruh <unruh@ut.ee> / hgweb
- Elimination of all z3 calls — paulson <lp15@cam.ac.uk> / hgweb
- Word_Lib sync from l4v; tweak word_eqI — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- generalise word_eqI method; make sure it is exercised — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- test_bit_size not longer needed; avoid potential nontermination — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Word_Lib tweaks for slightly more backwards compatibility — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- use bit_simps in word_eqI method — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adapted to new version of Infinite_Sum in isabelle-dev — Manuel Eberl <eberlm@in.tum.de> / hgweb
- avoid hardwired document output; — wenzelm / hgweb
- CTR and ETTS: integration with SpecCheck: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
- Complex_Bounded_Operators: Replaced use of HOL-Analysis.Infinite_Set_Sum by HOL-Analysis.Infinite_Sum — Dominique Unruh <unruh@ut.ee> / hgweb
- Banach_Steinhaus: Removed unused theory dependency Infinite_Set_Sum — Dominique Unruh <unruh@ut.ee> / hgweb
- merge — Burkhart Wolff <wolff@lri.fr> / hgweb
- merge — Burkhart Wolff <wolff@lri.fr> / hgweb
- Merge Isabelle_C: New C11_Ast_Lib Interface, improved API's, improved doc. — Burkhart Wolff <wolff@lri.fr> / hgweb
- documentation fine-tuning. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Added section on C11_Ast_Lib in chapter II. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Example section restored and Documentation adapted. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Stramge intermediate configuration: Example section zerschossen. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Port to Isabelle2021-1 RC 2. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Improved documentation. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Examples for iterator - applications: queries, and translations into term. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Rearranging standard root store; better documentation in C_Command. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Rearranging the ML _programming Example Section C1. — Burkhart Wolff <wolff@lri.fr> / hgweb
- reorg 1 — Burkhart Wolff <wolff@lri.fr> / hgweb
- ... — Burkhart Wolff <wolff@lri.fr> / hgweb
- Improved Standard Interface to C11: Better signatures, a CEnv signature, C11 Std Ast Store (in C2.thy) — Burkhart Wolff <wolff@lri.fr> / hgweb
- Restructuring of Interfaces; more show cases. — Burkhart Wolff <wolff@lri.fr> / hgweb
- Updated meta-data for Optics — Simon Foster <simon.foster@york.ac.uk> / hgweb
- Additional scene laws — Simon Foster <simon.foster@york.ac.uk> / hgweb
- Branch merge — Simon Foster <simon.foster@york.ac.uk> / hgweb
- 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
- feat(SpecCheck/Show) add parentheses for option SOME case — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- merged — desharna / hgweb
- weakened ordering requirements — desharna / hgweb
- used well-founded pre-order in standard redundancy criterions — desharna / hgweb
- derived refutational completeness from finitary and non-finitary standard redundancy criterion — desharna / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- 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 - factor_complex_poly delivers distinct list — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merged — paulson / hgweb
- Removal of material that's going to be in Isabelle2021-1 — paulson <lp15@cam.ac.uk> / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- refactoring (moving theories and lemmas around) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sync from l4v — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjusted Factor_Algebraic_Polynomial to Isabelle/devel (and Isabelle 2021-1, RC3) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge of afp-2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry PAL — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry Factor_Algebraic_Polynomial — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- document `publish -` — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- changed affiliation of eberl (this time properly) — Manuel Eberl <manuel@pruvisto.org> / hgweb
- changed affiliation of Eberl — Manuel Eberl <manuel@pruvisto.org> / hgweb
- sitegen for Real_Power — paulson <lp15@cam.ac.uk> / hgweb
- new entry Real_Power — paulson <lp15@cam.ac.uk> / hgweb
- New entry Szemeredi_Regularity — nipkow / hgweb
- tuned proofs -- avoid z3; — wenzelm / hgweb
#78 (Nov 14, 2021, 12:14:00 AM)
- merged — nipkow / hgweb
- tuned (thanks to J. Villadsen) — nipkow / hgweb
- added padding to Mirabelle's output — desharna / hgweb
- merged — desharna / hgweb
- tuned generation of TPTP with $ite/$let in higher-order logics — desharna / hgweb
- tuned generation of TPTP with $ite in function position — desharna / hgweb
- tuned TPTP generation of If helper facts — desharna / hgweb
- merged — wenzelm / hgweb
- clarified signature: prefer static operations; — wenzelm / hgweb
- clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified signature: more explicit class Entity_Context with private state + operations; — wenzelm / hgweb
- more hyperlinks, notably internal fact references; — wenzelm / hgweb
- Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO — paulson <lp15@cam.ac.uk> / hgweb
- A tiny bit of tidying connected with Zorn's Lemma — paulson <lp15@cam.ac.uk> / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- 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
- revert temporary workaround 6d111935299c; — wenzelm / hgweb
- added lemma — nipkow / hgweb
- merged — nipkow / hgweb
- tuned attributes to avoid looping — nipkow / hgweb
- added eq_iff_swap for creating symmetric variants of thms; applied it in List. — nipkow / hgweb
- tuned text; — wenzelm / hgweb
- more robust timeout, following df4449c6eff1; — wenzelm / hgweb
- more accurate Files.isRegularFile, exclude directories (e.g. jar_path); — wenzelm / hgweb
- proper java_version for isabelle_setup; — wenzelm / hgweb
- explicit option metric_argo_timeout, with reasonable default for Raspberry Pi; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- repackage minisat-2.2.1 with cygwin1.dll: required to run the executable without existing Cygwin context (normally provided by bash_process); — wenzelm / hgweb
- discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do; — wenzelm / hgweb
- clarified messages, depending on option "document_echo"; — wenzelm / hgweb
- just one cache, via HTML_Context, via Sessions.Store or Session; — wenzelm / hgweb
- merged — paulson / hgweb
- new lemmas about convex, concave functions, + tidying — paulson <lp15@cam.ac.uk> / hgweb
- proper support for arm64; — wenzelm / hgweb
- no perl (amending 59ef23ac81ab); — wenzelm / hgweb
- merged — wenzelm / hgweb
- Added tag Isabelle2021-1-RC2 for changeset b92b5a57521b — wenzelm / hgweb
- merged — nipkow / hgweb
- Preserve variable name z in VAR {z = t} — nipkow / hgweb
- back to scala-2.13.5: avoid crash of Scala REPL on arm64-darwin; — wenzelm / hgweb
- updated to polyml-5.9-5d4caa8f7148, which also contains ARM64 on darwin (unused by default); — wenzelm / hgweb
- more precise URL — nipkow / hgweb
- tuned page breaks — nipkow / hgweb
#78 (Nov 14, 2021, 12:14:00 AM)
- CTR and ETTS: integration with SpecCheck — user9716869 <user9716869@gmail.com> / hgweb
- used antiquotation to fix LaTeX failure — desharna / hgweb
- adapted to devel — nipkow / hgweb
- updated to devel — nipkow / hgweb
- merged — nipkow / hgweb
- tuned proof for devel — nipkow / hgweb
- clarified quotes vs. apostrophes vs. primes; — wenzelm / hgweb
- more accurate use of LaTeX ndash; — wenzelm / hgweb
- prefer portable LaTeX mdash; — wenzelm / hgweb
- tuned whitespace --- removed suspicious Unicode; — wenzelm / hgweb
- proper Unix linefeeds; — wenzelm / hgweb
- changed affiliation of eberl (this time properly) — Manuel Eberl <manuel@pruvisto.org> / hgweb
- changed affiliation of eberl — Manuel Eberl <manuel@pruvisto.org> / hgweb
- added author to Saturation_Framework_Extensions — desharna / hgweb
- derived calculus_with_standard_redundancy lemmas from calculus_with_finitary_standard_redundancy — desharna / hgweb
- added locale calculus_with_finitary_standard_redundancy — desharna / hgweb
- 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 - feat(SpecCheck) add better unit tests facilities, examples and exceptions property — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- discontinued somewhat pointless and slightly outdated document_preprocessor (after consultation with the author); — wenzelm / hgweb
- Correctness_Algebras: increase nitpick timeout — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- CZH: dagger monoidal categories — user9716869 <user9716869@gmail.com> / hgweb
- update it Isabelle/925b46043b84 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- merge from afp-2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- sitegen for Registers — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Registers — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
#77 (Nov 7, 2021, 12:14:00 AM)
- cover all possible kinds, notably for references outside of this theory (amending 129fb11b357f); — wenzelm / hgweb
- proper foundational order; — wenzelm / hgweb
- back to non-strict Export_Theory.read_theory (without warning): theories could have been skipped due to "condition"; — wenzelm / hgweb
- use all entity kinds from theory export, e.g. "method", "attribute"; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified physical_ref; — wenzelm / hgweb
- proper treatment of session build hierarchy; — wenzelm / hgweb
- proper used_theories for session build hierarchy, not known_theories from imported sessions; — wenzelm / hgweb
- present theories from imported sessions as required; — wenzelm / hgweb
- avoid multiple copies of fonts;
proper fonts prefix for aux. files; — wenzelm / hgweb - more compact persistent data; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- proper term_cache; — wenzelm / hgweb
- prefer "NAME|KIND" format, as already used in Isabelle/MMT and Isabelle/Dedukti; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- observer proper session hierarchy (according to build_graph): thus exported artifacts are always valid; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified order: prefer bottom-up construction of partial content; — wenzelm / hgweb
- more thorough update_global_index: overwrite old content; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified HTML_Context: just one context type; — wenzelm / hgweb
- unused (see also 217e6cf61453, 5e7916535860); — wenzelm / hgweb
- merged — wenzelm / hgweb
- 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 - tuned signature; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- proper support of verit's return code for timeout — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
- tuned whitespace; — wenzelm / hgweb
- updated to verit-2021.06.1-rmx, to address "Abnormal termination with exit code 14"; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- prefer official Export.explode_name;
avoid string interpolation: Isabelle/Scala is closer to Isabelle/ML than Python/Perl; — wenzelm / hgweb - tuned; — wenzelm / hgweb
- avoid conflict with future keyword; — wenzelm / hgweb
- tuned messages; — wenzelm / hgweb
- clarified signature: more direct XML.symbol_length; — wenzelm / hgweb
- more direct Symbol.length: Symbol.decode is redundant, symbol counts are invariant under it; — wenzelm / hgweb
- tuned -- eliminate clones stemming from d28a51dd9da6; — wenzelm / hgweb
- more to ANNOUNCE; — wenzelm / hgweb
- clarified link style: similar to Isabelle/jEdit; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- improved HTML presentation by Fabian Huch; — wenzelm / hgweb
- proper HTTPS; — wenzelm / hgweb
- proper markup type (amending be49c660ebbf); — wenzelm / hgweb
- merged; — wenzelm / hgweb
- more PIDE markup; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- more PIDE markup; — wenzelm / hgweb
- recover library_index_content.template from c337c798f64c: required for website/build/main; — wenzelm / hgweb
- merged — paulson / hgweb
- simplified some ugly proofs — paulson <lp15@cam.ac.uk> / hgweb
- more generous timeout: support build on Raspberry Pi; — wenzelm / hgweb
- add documentation for pred_mono — traytel / hgweb
- merged — desharna / hgweb
- added "mono" attribute to BNF generated pred_mono theorems — desharna / hgweb
- merged — desharna / hgweb
- do not declare $let-bound variables in TPTP output — desharna / hgweb
- IDE build actually works (but somewhat pointless); — wenzelm / hgweb
- suppress sources from jEdit/test, which prevent regular build of the generated scala_project; — wenzelm / hgweb
- removed junk; — wenzelm / hgweb
- improve pagebreaks by *not* using supertabular too much; — wenzelm / hgweb
- updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc; — wenzelm / hgweb
- more robust "isabelle scala_project": Gradle has been replaced by Maven; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- support linux_arm as well, e.g. native Docker on Apple Silicon; — wenzelm / hgweb
- update paths at TUM; — wenzelm / hgweb
- Added tag Isabelle2021-1-RC1 for changeset 81cc8f2ea9e7 — wenzelm / hgweb
- updated for release; — wenzelm / hgweb
- some reordering for release; — wenzelm / hgweb
- updated to jdk-17.0.1+12; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- minor performance tuning; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- provide native executables for arm64-darwin, for more robust startup without Rosetta 2; — wenzelm / hgweb
- tuned proofs -- avoid z3, which is unavailable on arm64-linux; — wenzelm / hgweb
- prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms; — wenzelm / hgweb
- discontinued pointless check of kodkodi_version, it is implicit in the bundled component; — wenzelm / hgweb
#77 (Nov 7, 2021, 12:14:00 AM)
- Correctness_Algebras: increase session timeout — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- tuned signature, according to Isabelle/df12779c3ce8; — wenzelm / hgweb
- feat(SpecCheck) add possibility to make builds fail on failure and extend README — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- added missing funding information — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- restored theory structure for simple genericity. — haftmann / hgweb
- Backed out changeset af549be0a8cd — haftmann / hgweb
- restored different entrance points a before Isabelle2021 — haftmann / hgweb
- proper parentheses (amending 354560d7143a); — wenzelm / hgweb
- Adjusted to prospective release Isabelle2021-2. — haftmann / hgweb
- Correctness_Algebras: uncomment counterexamples — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- clarified identity of theory data: avoid accidental pointer_eq, use equality on unique serial instead; — wenzelm / hgweb
- clarified identity of theory data: pointer_eq is not well-defined (and fails on ARM64), use equality on unique serial instead; — wenzelm / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- remove unused functions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- silence sitegen warning — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry X86_Semantics — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- adjust to isabelle@549019b4a808 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- metadata for Belief_Revision — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Belief_Revision — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- New entry Correctness_Algebras — nipkow / hgweb
- prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms; — wenzelm / hgweb
#76 (Oct 31, 2021, 12:14:00 AM)
- tuned proofs -- avoid z3, which is unavailable on arm64-linux; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- test version of prespective polyml-5.9; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- updated for pre-5.9 testing; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- more robust subgoal addressing; — wenzelm / hgweb
- proper subgoal addressing; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- recursive find_eq, not find_dist; — wenzelm / hgweb
- misc tuning and clarification; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- 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 - misc tuning and clarification; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta; — wenzelm / hgweb
- clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta; — wenzelm / hgweb
- avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570); — wenzelm / hgweb
- added Thm.instantiate_beta;
tuned; — wenzelm / hgweb - moved generic implementation into HOL-Main — haftmann / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- discontinued somewhat pointless antiquotations; — wenzelm / hgweb
- NEWS; — wenzelm / hgweb
- clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- support for "lemma";
support for "schematic" mode;
clarified error position; — wenzelm / hgweb - tuned; — wenzelm / hgweb
- local fixes for "lemma" antiquotation; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified keywords: major take precedence for commands, but not used for antiquotations;
clarified modules; — wenzelm / hgweb - tuned modules; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- moved a theorem to a sensible place — paulson <lp15@cam.ac.uk> / hgweb
- merged — wenzelm / hgweb
- tuned, continuing e955964d89cb; — wenzelm / hgweb
- avoid waste of resources due to dynamic simpset (amending 45c09620f726); — wenzelm / hgweb
- fix latex — Norbert Schirmer <nschirmer@apple.com> / hgweb
- clarified modules; — wenzelm / hgweb
- more generic bit/word lemmas for distribution — haftmann / hgweb
- merged — paulson / hgweb
- Added / moved some simple set-theoretic lemmas — paulson <lp15@cam.ac.uk> / hgweb
- more CONTRIBUTORS and NEWS; — wenzelm / hgweb
- cleanup; add Apple reference — Norbert Schirmer <nschirmer@apple.com> / hgweb
- refine interface — Norbert Schirmer <nschirmer@apple.com> / hgweb
- generalized component lookup for syntax and distinctness proofs. added some tracing. — Norbert Schirmer <nschirmer@apple.com> / hgweb
- merged — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more robust: genuinely free variables need to be instantiated; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- clarified errors; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature -- avoid clones; — wenzelm / hgweb
- Refinement of partitions — paulson <lp15@cam.ac.uk> / hgweb
- avoid persistence of static context: instantiation arguments should provide proper dynamic context; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more markup; — wenzelm / hgweb
- clarified name, syntax, messages; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more control symbols; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- ML antiquotations to instantiate types/terms/props; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- discontinued obsolete "val extend = I" for data slots; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified keywords and reports; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- merged — desharna / hgweb
- proper veriT --max-time option — desharna / hgweb
- refactored tptp_builtins in Sledgehammer — desharna / hgweb
- merged — wenzelm / hgweb
- tuned ML --- clarified use of context;
tuned message; — wenzelm / hgweb - tuned --- fewer clones; — wenzelm / hgweb
- updated to jEdit plugin Highlight 2.5; — wenzelm / hgweb
- proper tactic combinator; — wenzelm / hgweb
- proper file headers; — wenzelm / hgweb
- clarified context;
clarified modules; — wenzelm / hgweb - more accurate treatment of context; — wenzelm / hgweb
- updated email address — Manuel Eberl <manuel@pruvisto.org> / hgweb
- removed some 'private' modifiers from HOL-Computational_Algebra — Manuel Eberl <manuel@pruvisto.org> / hgweb
- merged — wenzelm / hgweb
- merged — wenzelm / hgweb
- more robust Variable.revert_bounds (see also b12f2cef3ee5); — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- tuned -- proper names/scopes for contexts; — wenzelm / hgweb
- clarified context; — wenzelm / hgweb
- clarified context; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- more accurate treatment of context;
declare generated bounds for the sake of recdef, which has variables leaking from local context; — wenzelm / hgweb - isabelle regenerate_cooper; — wenzelm / hgweb
- revert bbfed17243af, breaks HOL-Proofs extraction; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- proper p' instead of p (amending 52c7c42e7e27); — wenzelm / hgweb
- proper context for Goal.prove_internal; — wenzelm / hgweb
- 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 - more accurate treatment of context, notably for nested Goal.proof / SUBPROOF; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- spelling; — wenzelm / hgweb
- clarified context; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned Vampire configuration to use TFX in Sledgehammer — desharna / hgweb
#76 (Oct 31, 2021, 12:14:00 AM)
- updated metadata for Count_Complex_Roots — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- corrected the timeout for CZH_Universal_Constructions — user9716869 <user9716869@gmail.com> / hgweb
- CZH: further results about comma categories and Kan extensions, a variety of other minor amendments — user9716869 <user9716869@gmail.com> / hgweb
- more generic bit/word lemmas for distribution — haftmann / hgweb
- Fixing a name clash between two different "restrict" operators — paulson <lp15@cam.ac.uk> / hgweb
- Merged — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- solved the roots-on-the-border problem — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- split Count_Complex_Roots — Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> / hgweb
- more realistic timeout; — wenzelm / hgweb
- clarified signature, according to Isabelle/ccf599864beb; — wenzelm / hgweb
- back to dedicated separate shift operations for infix syntax;
more default simp rules on closed numeric expressions — haftmann / hgweb - modify JinjaDCI — nanjiang <nanjiang@whu.edu.cn> / hgweb
- modify JinjaDCI — nanjiang <nanjiang@whu.edu.cn> / hgweb
- Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Various tuning that for some reason didn't get merged from my master branch. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- A spot of polishing — paulson <lp15@cam.ac.uk> / hgweb
- Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Update metadata to reflect changes made in July, 2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Add a revision note concerning material added in July, 2021. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- tuned signature, according to Isabelle/042041c0ebeb; — wenzelm / hgweb
- Merged. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- Sync with my development repo. — Eugene W. Stark <stark@cs.stonybrook.edu> / hgweb
- 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 - discontinued obsolete "val extend = I" for data slots; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- merged — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
- metadata update for MFODL_Monitor_Optimized — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
- fixed a mistake in MFODL_Monitor_Optimized — Joshua Schneider <joshua.schneider@inf.ethz.ch> / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- adjusted Virtual-Substitution from 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge of AFP 2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- fixed duplicate "and" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Virtual_Substitution — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Virtual Substitution — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- updated website/email address — Manuel Eberl <manuel@pruvisto.org> / hgweb
- modifications in Jinja and DOminance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
- modifications in Jinja and Dominance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
- modifications in Jinja and Dominance_CHK — nanjiang <nanjiang@whu.edu.cn> / hgweb
- merged — wenzelm / hgweb
- adapted to Term.dest_abs_global / Logic.dest_all_global (e.g. Isabelle/f07761ee5a7f); — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- tuned -- proper names/scopes for contexts; — wenzelm / hgweb
- tuned proofs; — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- more accurate treatment of context; — wenzelm / hgweb
- proper antiquotations; — wenzelm / hgweb
- tuned messages; — wenzelm / hgweb
- more maintainable Isabelle/ML: proper signatures, proper names/scopes for contexts;
tuned whitespace; — wenzelm / hgweb - dead code!? — wenzelm / hgweb
- clarified signature, following Isabelle/de4f151c2a34; — wenzelm / hgweb
#75 (Oct 24, 2021, 12:14:00 AM)
- added Mirabelle action presburger — desharna / hgweb
- added timing to Mirabelle action arith — desharna / hgweb
- added error message on invalid Mirabelle action — desharna / hgweb
#75 (Oct 24, 2021, 12:14:00 AM)
- CZH: large limits, generalizations, a variety of minor amendments — user9716869 <user9716869@gmail.com> / hgweb
#74 (Oct 17, 2021, 12:14:00 AM)
- A few new lemmas plus some refinements — paulson <lp15@cam.ac.uk> / hgweb
- merged — desharna / hgweb
- produced Mirabelle output directly in ML until Scala output gets fixed — desharna / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- removed unused material (left-over from fd0c85d7da38); — wenzelm / hgweb
- support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a); — wenzelm / hgweb
- removed junk; — wenzelm / hgweb
- merged — nipkow / hgweb
- separated commands from annotations to be able to abstract about the latter only — nipkow / hgweb
- prefer standard Term.dest_abs, with minor deviation of generated names; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- more examples — nipkow / hgweb
- 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
- more complete simp rules — haftmann / hgweb
- more complete simp rules — haftmann / hgweb
- avoid overaggressive contraction of conversions — haftmann / hgweb
- normalizing NOT (numeral _) (again) — haftmann / hgweb
#74 (Oct 17, 2021, 12:14:00 AM)
- Simplified a definition — paulson <lp15@cam.ac.uk> / hgweb
- modify propa — nanjiang <nanjiang@whu.edu.cn> / hgweb
- bit singleton shifts recovered for the sake of backward compatibility — haftmann / hgweb
- updated to 7422950f3955 — nipkow / hgweb
- merge — Alexander Bentkamp <a.bentkamp@vu.nl> / hgweb
- EPO: simplify proof — Alexander Bentkamp <a.bentkamp@vu.nl> / hgweb
- primer — haftmann / hgweb
- more complete simp rules — haftmann / hgweb
- more complete simp rules (examples) — haftmann / hgweb
- avoid overaggressive contraction of conversions — haftmann / hgweb
- slightly more prominence for proof tools; more examples — haftmann / hgweb
#73 (Oct 10, 2021, 12:14:00 AM)
- tuned text; — wenzelm / hgweb
- recover NEWS from 78d1f73bbeaa; — wenzelm / hgweb
- save 90 MB by excluding rlwrap and thus perl; — wenzelm / hgweb
- save 45 MB by excluding rlwrap and thus perl; — wenzelm / hgweb
- NEWS; — wenzelm / hgweb
- clarified test of directories; — wenzelm / hgweb
- misc tuning for release; — wenzelm / hgweb
- merged — wenzelm / hgweb
- updated to kodkodi-1.5.7. with more robust/portable management of files and processes; — wenzelm / hgweb
- provide minisat-2.2.1 on all currently supported platforms, notably as external solver for Nitpick; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- proper build on macOS; — wenzelm / hgweb
- build minisat, using recent fork from original sources; — wenzelm / hgweb
- proper platform_path for executables run from Java; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- merged — desharna / hgweb
- added timeout to veriT — desharna / hgweb
- new notion of infinite sums in HOL-Analysis, ordering on complex numbers — eberlm <eberlm@in.tum.de> / hgweb
- NEWS and CONTRIBUTORS — desharna / hgweb
- merged — desharna / hgweb
- added offset to Mirabelle's tptp output names — desharna / hgweb
- tuned zipperposition config in sledgehammer — desharna / hgweb
- considered slices overhead in sledgehammer — desharna / hgweb
- tuned atp_prover sliding — desharna / hgweb
- tuned Zipperposition slides in sledgehammer — desharna / hgweb
- include arm64-linux; — wenzelm / hgweb
- updated to Vampire 4.6, as proposed by Martin Desharnais; — wenzelm / hgweb
- build from official downloads; — wenzelm / hgweb
- build just one vampire version; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- maintain previous theory identifier to support semantic caching, notably in Isabelle/Naproche; — wenzelm / hgweb
- more exports, notably for Isabelle/Naproche; — wenzelm / hgweb
- include arm64-linux; — wenzelm / hgweb
- prefer existing OCaml installation; — wenzelm / hgweb
- include arm64-linux; — wenzelm / hgweb
- no patchelf on macOS (undetected due to cached executables?); — wenzelm / hgweb
- provide opam-2.1.0 for experimentation; — wenzelm / hgweb
- rebuild cygwin-20211004.tar.gz; — wenzelm / hgweb
- include arm64-linux; — wenzelm / hgweb
- updated to cygwin-20211004: build again; — wenzelm / hgweb
- merged — wenzelm / hgweb
- removed pointless NEWS: both Docker/ubuntu and Cygwin provide perl by default; — wenzelm / hgweb
- actually use cygwin-20211002 (amending ff0ca375457c); — wenzelm / hgweb
- discontinued perl; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- proper term operation Term.dest_abs; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned proofs;
fewer warnings; — wenzelm / hgweb - more standard binder syntax; — wenzelm / hgweb
- clarified 'let' syntax: avoid conflict with existing 'let' in FOL; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- merged — paulson / hgweb
- removal of a redundant theorem (and white space) — paulson <lp15@cam.ac.uk> / hgweb
- new material from the Roth development, mostly about finite sets, disjoint famillies and partitions — paulson <lp15@cam.ac.uk> / hgweb
- clarified and updated for release; — wenzelm / hgweb
- formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc; — wenzelm / hgweb
- more NEWS and CONTRIBUTORS; — wenzelm / hgweb
- clarified comments; — wenzelm / hgweb
- support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing); — wenzelm / hgweb
- clarified dependencies; — wenzelm / hgweb
- updated for release; — wenzelm / hgweb
- Added tag Isabelle2021-1-RC0 for changeset fedc0b659881 — isatest / hgweb
- provide Isabelle/jEdit plugins as services, and thus allow user components do the same; — wenzelm / hgweb
- merged — wenzelm / hgweb
- updated for release; — wenzelm / hgweb
- misc tuning for release; — wenzelm / hgweb
- update dependency; — wenzelm / hgweb
- trim whitespace; — wenzelm / hgweb
- misc tuning for release; — wenzelm / hgweb
- misc tuning for release; — wenzelm / hgweb
- isabelle build_components -u; — wenzelm / hgweb
- updated to Haskell Stach lts-18.12 with GHC ghc-8.10.7; — wenzelm / hgweb
- updated to current Cygwin, near 3.2.0;
discontinued perl; — wenzelm / hgweb - updated to sumatra_pdf-3.3.3; — wenzelm / hgweb
- updated default version; — wenzelm / hgweb
- updated to xz-java-1.9; — wenzelm / hgweb
- updated to sqlite-jdbc-3.36.0.3; — wenzelm / hgweb
- updated to postgresql-42.2.24; — wenzelm / hgweb
- updated to jfreechart-1.5.3; — wenzelm / hgweb
- updated to flatlaf-1.6; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax; — wenzelm / hgweb
- clarified sledgehammer_provers, following d8dc8fdc46fc; — wenzelm / hgweb
- proper term operation Term.dest_abs; — wenzelm / hgweb
- tuned, following Syntax_Trans.variant_abs; — wenzelm / hgweb
- proper patterns for (- numeral t), amending 03ff4d1e6784; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- merged — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
- update syntax for verit — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- provide verit-2021.06-rmx; — wenzelm / hgweb
#73 (Oct 10, 2021, 12:14:00 AM)
- ETTS: minor amendments — user9716869 <user9716869@gmail.com> / hgweb
- CTR and ETTS: integration with fd5f62176987 — user9716869 <user9716869@gmail.com> / hgweb
- adapted QHLProver to isabelle-dev/409ca22dee4c — Manuel Eberl <eberlm@in.tum.de> / hgweb
- adapted to isabelle-dev/409ca22dee4c — Manuel Eberl <eberlm@in.tum.de> / hgweb
- adapted to devel — nipkow / hgweb
- Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Weighted_Path_Order: update to isabelle@ffb15f7f26d5 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add missing session dependency — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry FOL_Axiomatic — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- regen website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- minor editorial changes for CZH entries — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- New entry Weighted_Path_Order — nipkow / hgweb
- fxed metadata (forgot .html) in link — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata and sitegen for complex bounded operators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Complex_Bounded_Operators — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- restructure resultant algorithms, so that tuned code-equations are also availalbe for integral domains — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- removed obselete sorted_sorted_wrt, following Isabelle/06aeb9054c07; — wenzelm / hgweb
- clarified timeout;
tuned whitespace; — wenzelm / hgweb - hide_lams ~> opaque_lifting; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- proper inst table; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- proper inst table; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- proper match against const_name; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- fix(ci): clarified addresses, set proper TLS version; — Fabian Huch <huch@in.tum.de> / hgweb
- feat(ci): remove hard-coded address; — Fabian Huch <huch@in.tum.de> / hgweb
- feat(SpecCheck/Show) tune pretty printing for environments — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- eliminated intermediate sessions "Pre-BZ" and "JNF-AFP-Lib" — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- 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 - New entry: Dominance_CHK — nipkow / hgweb
- Schutz_Spacetime website — paulson <lp15@cam.ac.uk> / hgweb
- new entry Schutz_Spacetime — paulson <lp15@cam.ac.uk> / hgweb
- metadata for Logging_Independent_Anonymity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Logging_Independent_Anonymity — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
#72 (Oct 3, 2021, 12:14:00 AM)
- clarified antiquotations; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified antiquotations;
some comments concerning odd "- numeral"; — wenzelm / hgweb - clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- merged — desharna / hgweb
- tuned TPTP parsing of THF function application — desharna / hgweb
- clarified examples; — wenzelm / hgweb
- repaired slip — haftmann / hgweb
- merged — desharna / hgweb
- updated to Zipperposition 2.1 — desharna / hgweb
- fixed veriT environment variable in sledgehammer's documentation — desharna / hgweb
- avoid overlapping PIDE markup (amending bb25ea271b15); — wenzelm / hgweb
- recover some Linux test, using virtual machine node (Ubuntu 20.04, 4 cores, 16 GB); — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified positions, notably for ML compiler errors; — wenzelm / hgweb
- clarified message; — wenzelm / hgweb
- proper default for Sledgehammer GUI panel; — wenzelm / hgweb
- tuned antiquotations; — wenzelm / hgweb
- more convenient ML arguments: avoid excessive nesting of cartouches; — wenzelm / hgweb
- outer syntax: support for control-cartouche tokens; — wenzelm / hgweb
- merged — nipkow / hgweb
- An example — nipkow / hgweb
- prefer veriT over Z3 in sledgehammer — desharna / hgweb
- added Zipperposition to sledgehammer's default provers — desharna / hgweb
- provide zipperposition-2.1 (still unused); — wenzelm / hgweb
- tuned docs — blanchet / hgweb
- merged — wenzelm / hgweb
- improper proof command 'guess' moved to separate theory "Pure-ex.Guess"; — wenzelm / hgweb
- NOT is part of syntax bundle also — haftmann / hgweb
#72 (Oct 3, 2021, 12:14:00 AM)
- repaired slip — haftmann / hgweb
- feat(SpecCheck) folder renaming, types for tests — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- tuned — nipkow / hgweb
- 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)
- merged — wenzelm / hgweb
- tuned proofs --- avoid 'guess'; — wenzelm / hgweb
- apply declarations from interpretations in eigen context also — haftmann / hgweb
- grant access to sun.tools.jconsole, as required for Java 17; — wenzelm / hgweb
- update to e-2.6, following Martin Desharnais; — wenzelm / hgweb
- updated to Metis 2.4 (release 20200713) — desharna / hgweb
- avoid problems with launch4j and jdk-17; — wenzelm / hgweb
- update to jdk-17+35 (LTS); — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- unused since 398b7bb9ebdd; — wenzelm / hgweb
- merged — desharna / hgweb
- removed checks for non-commercial usage of Vampire as it is now under BSD licence — desharna / hgweb
- enabled FOOL for Vampire in Sledgehammer — desharna / hgweb
- used Vampire 4.5.1 in Sledgehammer — desharna / hgweb
- proper NEWS; — wenzelm / hgweb
- tuned NEWS; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- clarified partial application: immediate check of object-logic, and avoidance of context within closure; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified antiquotations; — wenzelm / hgweb
- ML antiquotations for object-logic judgment; — wenzelm / hgweb
- proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- more uniform syntax; — wenzelm / hgweb
- permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone; — wenzelm / hgweb
- NEWS; — wenzelm / hgweb
- bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; — wenzelm / hgweb
- localized command 'syntax' and 'no_syntax'; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- merged — desharna / hgweb
- proper constants in TPTP $let binding — desharna / hgweb
- more operations from Isabelle/ML; — wenzelm / hgweb
- merged — wenzelm / hgweb
- tuned proofs --- eliminated 'guess'; — wenzelm / hgweb
- tuned proofs;
tuned whitespace; — wenzelm / hgweb - clarified antiquotations; — wenzelm / hgweb
- proper firstorderization in Sledgehammer — desharna / hgweb
- clarified signature;
clarified antiquotations; — wenzelm / hgweb - clarified antiquotations; — wenzelm / hgweb
- clarified signature -- prefer antiquotations (with subtle change of exception content); — wenzelm / hgweb
- more control symbols; — wenzelm / hgweb
- support ML antiquotations with fn abstraction; — wenzelm / hgweb
- unused; — wenzelm / hgweb
#71 (Sep 26, 2021, 12:14:00 AM)
- ported Design-Theory from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- ported Three-Circles from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- ported Cubic_Quartic_Equations from AFP 2021 to devel — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- merge of AFP 2021 — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- Cubic_Quartic_Equations sitegen — paulson <lp15@cam.ac.uk> / hgweb
- new entry Cubic_Quartic_Equations — paulson <lp15@cam.ac.uk> / hgweb
- sitegen for combinatorial design theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Combinatorial Design Theory — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Three Circles — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Three Circles — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- clarified modules, according to Isabelle/534b231ce041; — wenzelm / hgweb
- 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 - clarified signature, according to Isabelle/d882abae3379; — wenzelm / hgweb
#70 (Sep 19, 2021, 12:14:00 AM)
- clarified operations: follow Isabelle/ML more closely; — wenzelm / hgweb
- provide current vampire-4.5.1: presently unused in Sledgehammer, but relevant for Isabelle/Naproche; — wenzelm / hgweb
- obsolete; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified name and options for old vampire-4.2.2; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell) — haftmann / hgweb
- more latex macros; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more antiquotations;
more formal use of consts; — wenzelm / hgweb - more antiquotations;
more formal use of consts; — wenzelm / hgweb - clarified antiquotations; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- clarified antiquotation; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- ML antiquotations for type constructors and term constants; — wenzelm / hgweb
- more antiquotations; — wenzelm / hgweb
#70 (Sep 19, 2021, 12:14:00 AM)
- explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell) — haftmann / hgweb
- tuned signature, according to Isabelle/28a582aa25dd; — wenzelm / hgweb
#69 (Sep 12, 2021, 12:14:00 AM)
- tuned; — wenzelm / hgweb
- NEWS; — wenzelm / hgweb
- miscellaneous examples and experiments for Isabelle/Pure; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference); — wenzelm / hgweb
- NEWS; — wenzelm / hgweb
- clarified signature: more scalable operations; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- clarified order of extra type variables, following names more often than occurrences; — wenzelm / hgweb
- clarified signature;
tuned; — wenzelm / hgweb - tuned; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- more robust: client could have terminated already; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified set of items with order of addition; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- clarified signature;
clarified modules; — wenzelm / hgweb - tuned; — wenzelm / hgweb
- simplified: uniqueness check happens in export_consumer; — wenzelm / hgweb
- more markup, e.g. to locate defining theory node in formal document output; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- export other entities, e.g. relevant for formal document output;
clarified markup kind (PIDE) vs. export kind (e.g. MMT); — wenzelm / hgweb - pointer_eq_ord: minor performance tuning; — wenzelm / hgweb
- more robust: progress.stopped means that build has failed; — wenzelm / hgweb
- more reactive interrupt; — wenzelm / hgweb
- more reactive interrupt; — wenzelm / hgweb
- more robust: retain length of results; — wenzelm / hgweb
- more reactive interrupt; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified signature;
minor performance tuning; — wenzelm / hgweb - more scalable operations; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- more efficient operations: traverse hyps only when required; — wenzelm / hgweb
- more robust signature: result has no particular order; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- clarified; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- more scalable operations;
tuned; — wenzelm / hgweb - more scalable operations; — wenzelm / hgweb
- white space — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- some fixes connected with card_Diff_singleton — paulson <lp15@cam.ac.uk> / hgweb
- strengthened a few lemmas about finite sets and added a code equation for complex_of_real — paulson <lp15@cam.ac.uk> / hgweb
- tuned; — wenzelm / hgweb
- proper inst table; — wenzelm / hgweb
- more scalable data structure (but: rarely used many arguments); — wenzelm / hgweb
- minor performance tuning: fewer allocations;
clarified theory context; — wenzelm / hgweb
#69 (Sep 12, 2021, 12:14:00 AM)
- eliminated Specification.definition', following Isabelle/6876e3d5e362; — wenzelm / hgweb
- clarified signature: more scalable operations, according to Isabelle/c2ee8d993d6a; — wenzelm / hgweb
- clarified signature, according to Isabelle/612b7e0d6721; — wenzelm / hgweb
- tuned signature, according to Isabelle/839a6e284545; — wenzelm / hgweb
- merged — sterraf / hgweb
- Backed out changeset ef19e4e58b8c
restoring old argument order on synthesized formulas — sterraf / hgweb - avoid hardwired document; — wenzelm / hgweb
- merged — wenzelm / hgweb
- tuned signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
- clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
- clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
- clarified signature, according to Isabelle/9d9e7ed01dbb; — wenzelm / hgweb
- simplified, using Isabelle/ML operations; — wenzelm / hgweb
- adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for vars; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- more scalable operations; — wenzelm / hgweb
- merged — sterraf / hgweb
- synthesized formulas have their variables permuted — sterraf / hgweb
- merged — paulson / hgweb
- fixes for cardinality lemmas — paulson <lp15@cam.ac.uk> / hgweb
- proper inst table; — wenzelm / hgweb
#68 (Sep 5, 2021, 12:14:00 AM)
- tuned; — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- more Isabelle/Haskell operations;
tuned; — wenzelm / hgweb - avoid change of existing file, notably rebuild via ghc_stack; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- clarified process description; — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
#67 (Aug 29, 2021, 12:14:00 AM)
- more Isabelle/Haskell; — wenzelm / hgweb
- made sure lambda-lifting works well with native let binders in Sledgehammer — blanchet / hgweb
- handle Zipperposition's ResourceOut gracefully — blanchet / hgweb
- disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax — blanchet / hgweb
- proper test for type constructor; — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- merged — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more scalable data structure (but: rarely used with > 5 arguments); — wenzelm / hgweb
- Backed out changeset d4af818e0880 — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- merged — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- reflect moved theories — nipkow / hgweb
- unhide canonical function def examples — nipkow / hgweb
- merged — nipkow / hgweb
- merged — nipkow / hgweb
- Backed out changeset fe8d0f4da0e6 — nipkow / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- more Isabelle/Haskell operations; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- minor performance tuning; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- treat Symbol.eof as in ML (but: presently unused); — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- minor performance tuning; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- proper Isabelle symbol positions; — wenzelm / hgweb
- more Haskell operations; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned signature: prefer existing Haskell operations; — wenzelm / hgweb
- more Haskell operations; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- consolidation of rules for bit operations — haftmann / hgweb
#67 (Aug 29, 2021, 12:14:00 AM)
- Graphic rendering of Relational_Method PDF files refined. — Pasquale Noce <pasquale.noce@hidglobal.com> / hgweb
- Entry Relational_Method updated. — Pasquale Noce <pasquale.noce@hidglobal.com> / hgweb
- more realistic timeout; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- follow Isabelle/53e28c438f96; — wenzelm / hgweb
- clarified signature, following Isabelle/a3b0fc510705; — wenzelm / hgweb
- merged — nipkow / hgweb
- tuned — nipkow / hgweb
- consolidation of rules for bit operations — haftmann / hgweb
#66 (Aug 22, 2021, 12:14:00 AM)
- fixed $ite syntax in TPTP TFX generation — desharna / hgweb
- more Haskell operations; — wenzelm / hgweb
- merged — wenzelm / hgweb
- revert 0faa68dedce5: very slow; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- add/rename some theorems about Map(pings) — Lukas Stevens <mail@lukas-stevens.de> / hgweb
- support configuration options "show_results"; — wenzelm / hgweb
- consolidate_body more thoroughly, e.g. for reduced ML_Heap.obj_size; — wenzelm / hgweb
- merged — desharna / hgweb
- fixed $ite syntax in TPTP THX generation — desharna / hgweb
- tuned signature; — wenzelm / hgweb
- more scalable data structures; — wenzelm / hgweb
- more scalable data structures; — wenzelm / hgweb
- more scalable data structures;
tuned; — wenzelm / hgweb - proper position information for Context.theory_data_size; — wenzelm / hgweb
#66 (Aug 22, 2021, 12:14:00 AM)
- tuned name — nipkow / hgweb
- Fix typo — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
- Tune references
... using new name of BD_Security_Compositional — Thomas Bauereiss <thomas@bauereiss.name> / hgweb - Remove redundant license — Thomas Bauereiss <thomas@bauereiss.name> / hgweb
- more realistic timeout: approx. 5min CPU time; — wenzelm / hgweb
- cleaning up — nipkow / hgweb
- New entry CoSMeDis — nipkow / hgweb
- New entry CoSMed — nipkow / hgweb
- New entry: BD_Security_Compositional — nipkow / hgweb
- New entry: CoCon — nipkow / hgweb
- updated to devel — nipkow / hgweb
- merge from AFP 2021 — nipkow / hgweb
- New entry Fresh_Identifiers — nipkow / hgweb
- New entry: Relational_Forests — nipkow / hgweb
- cleaning up — nipkow / hgweb
- merged — nipkow / hgweb
- cleaning up — nipkow / hgweb
- 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 - tuned signature, following Isabelle/069f6b2c5a07; — wenzelm / hgweb
#65 (Aug 15, 2021, 12:14:00 AM)
- provide bash_process server for Isabelle/ML and other external programs;
clarified signature for Bash.params; — wenzelm / hgweb - clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- proper prover_options for batch-build; — wenzelm / hgweb
- clarified signature;
clarified errors; — wenzelm / hgweb - clarified signature: more options for bash_process; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- follow phabricator 2021 Week 26;
follow arcanist 2021 Week 23; — wenzelm / hgweb - tuned signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- type classes for XML data representation; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified types: prefer Isabelle byte strings; — wenzelm / hgweb
- merged — desharna / hgweb
- added option labels to Mirabelle actions — desharna / hgweb
- more operations: dest binders; — wenzelm / hgweb
- clarified abstract and concrete boolean algebras — haftmann / hgweb
- antiquotation for bundles — haftmann / hgweb
- prefer persistent hash code for cachable items (see also 72b13af7f266); — wenzelm / hgweb
- merged — wenzelm / hgweb
- more operations: record overall exported entities; — wenzelm / hgweb
- merged — desharna / hgweb
- added dummy_fof prover to Sledgehammer — desharna / hgweb
- fixed malconfigured option output_dir in mirabelle — desharna / hgweb
- merged — wenzelm / hgweb
- clarified export of formal entities: name space info is always present, but content depends on option "export_theory"; — wenzelm / hgweb
- proper name space "kind": this is a formal name, not comment; — wenzelm / hgweb
- more uniform signatures in ML and Scala; — wenzelm / hgweb
- merged — desharna / hgweb
- fixed typo — desharna / hgweb
- added dummy_thf prover to Sledgehammer — desharna / hgweb
- simplified hierarchy of type classes for bit operations — haftmann / hgweb
- obsolete — haftmann / hgweb
- more operations, notably free and bound variables as in Isabelle/Pure; — wenzelm / hgweb
- more operations on types and terms;
abstract syntax operations for Pure and HOL; — wenzelm / hgweb - clarified jEdit java sources; — wenzelm / hgweb
- clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for unknown reasons; — wenzelm / hgweb
- removed junk; — wenzelm / hgweb
- moved theory Bit_Operations into Main corpus — haftmann / hgweb
- more operations; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- organize syntax for word operations in bundles — haftmann / hgweb
- support for Lazy.Text; — wenzelm / hgweb
- prefer compact Isabelle.Bytes; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature --- more operations; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified order of modules; — wenzelm / hgweb
- more operations; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
#65 (Aug 15, 2021, 12:14:00 AM)
- metadata update for MFMC_Countable — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- derive rel_pmf characterization from bounded and unbounded MFMC theorem — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- drop boundedness requirement for the sink — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- avoid global tmp file: pointless due to implicit theory export; — wenzelm / hgweb
- repaired syntax — haftmann / hgweb
- tuned signature, following Isabelle/d030b988d470; — wenzelm / hgweb
- generalized gt_rat_sign_change to square-free polynomials — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- minor updates to bibliography — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- clarified signature; — wenzelm / hgweb
- clarified abstract and concrete boolean algebras — haftmann / hgweb
- antiquotation for bundles — haftmann / hgweb
- simplified hierarchy of type classes for bit operations — haftmann / hgweb
- restored executable conversions — haftmann / hgweb
- dropped junk — haftmann / hgweb
- moved theory Bit_Operations into Main corpus — haftmann / hgweb
- organize syntax for word operations in bundles — haftmann / hgweb
- more systematic approach for instantiation — haftmann / hgweb
- avoid seemingly unused transfer rules — haftmann / hgweb
#63 (Aug 1, 2021, 12:14:00 AM)
- clarified signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- merged — wenzelm / hgweb
- prefer Isabelle.Bytes, based on ShortByteString; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned signature: more generic operations; — wenzelm / hgweb
- prefer UTF8 implementation from Data.Text.Encoding (foreign C);
clarified signatures and modules; — wenzelm / hgweb - documented Mirabelle_Sledgehammer's new keep semantics — desharna / hgweb
- changed Mirabelle_Sledgehammer keep option from path to boolean — desharna / hgweb
- added automatic uniform stride option to Mirabelle — desharna / hgweb
- fixed HOL-ex following a5bab59d580b — desharna / hgweb
- added support for TFX $let to Sledgehammer's TPTP output — desharna / hgweb
- merged — desharna / hgweb
- fixed TFX generation when universal quantifier is used as term — desharna / hgweb
- merged — wenzelm / hgweb
- various improvements of "isabelle scala_project"; — wenzelm / hgweb
- support for native symlinks on Windows; — wenzelm / hgweb
- tuned Mirabelle's theory selection — desharna / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- updated for Isabelle2021 release; — wenzelm / hgweb
- back to stackage lts-17.10, to make this work on vmnipkow9 (Windows Server 2012 R2); — wenzelm / hgweb
- update to Haskell stack-2.7.3 and stackage lts-17.15; — wenzelm / hgweb
- clarified version: Apple now counts like 11, 12, ...; — wenzelm / hgweb
#63 (Aug 1, 2021, 12:14:00 AM)
- cleaner presentation of analysis theorems in preliminaries — yonoteam / hgweb
- Update to new Epistemic_Logic.thy — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Avoid typedefs — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Clean: set AFP standard document options — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Clean: re-add to chapter AFP — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Finitely_Generated_Abelian_Groups website — paulson <lp15@cam.ac.uk> / hgweb
- new entry Finitely_Generated_Abelian_Groups — paulson <lp15@cam.ac.uk> / hgweb
- Added Finitely_Generated_Abelian_Groups to metadata — Manuel Eberl <eberlm@in.tum.de> / hgweb
#62 (Jul 25, 2021, 12:14:00 AM)
- clarified signature; — wenzelm / hgweb
- clarified compiler output: allow multithreaded execution; — wenzelm / hgweb
- clarified signature: more operations; — wenzelm / hgweb
- clarified props: more permissive; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- clarified properties: "module" and "no_build";
clarified signature; — wenzelm / hgweb - clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- tuned document; — wenzelm / hgweb
- clarified names (again), e.g. relevant for "Plugin Options"; — wenzelm / hgweb
- added simp_options to meson — desharna / hgweb
- tuning — blanchet / hgweb
- parse TPTP operator @ also when not parenthesized — blanchet / hgweb
- removed setup for outdated CVC3 from Isabelle — blanchet / hgweb
- tuned E's lambda encoding — blanchet / hgweb
- use Vampire's clausifier with iProver, now that E's is no longer supported — blanchet / hgweb
- updated Sledgehammer docs -- removed most version numbers since these are tedious to maintain — blanchet / hgweb
- compile — blanchet / hgweb
- tuned; — wenzelm / hgweb
- NEWS; — wenzelm / hgweb
- updated documentation on Isabelle/Scala; — wenzelm / hgweb
- discontinued obsolete Apple (deprecated); — wenzelm / hgweb
- clarified component setup: exclude jar from active component, but use sources from template within ISABELLE_HOME (relevant for "isabelle scala_project -L"); — wenzelm / hgweb
- more robust "isabelle build_scala" as separate tool; — wenzelm / hgweb
- tuned --- based on hints by IntelliJ IDEA; — wenzelm / hgweb
- more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in AFP/1001c0dfced0); — wenzelm / hgweb
- more portable across history; — wenzelm / hgweb
- proper isabelle.setup.Setup build; — wenzelm / hgweb
- rebuild component; — wenzelm / hgweb
- more complete scala_project, including Isabelle/jEdit plugins; — wenzelm / hgweb
- clarified directories; — wenzelm / hgweb
- more accurate scala_project, based on build.props of components; — wenzelm / hgweb
- clarified build_props: empty module means no build;
clarified signature;
clarified errors; — wenzelm / hgweb - tuned; — wenzelm / hgweb
- CONTRIBUTORS — haftmann / hgweb
- merged — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- rebuild component; — wenzelm / hgweb
- more robust: for the sake of Isabelle.app on macOS; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- rebuild component; — wenzelm / hgweb
- more informative errors: capture low-level compiler output; — wenzelm / hgweb
- more direct isabelle_scala_build: always enabled, no "Admin" requirement; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- clarified names; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- clarified directory; — wenzelm / hgweb
- clarified names; — wenzelm / hgweb
- clarified component setup for old graph browser; — wenzelm / hgweb
- redundant: *.class and *.jar are already ignored; — wenzelm / hgweb
- proper cat_lines: avoid last "\n"; — wenzelm / hgweb
- merged — paulson / hgweb
- A few new lemmas and simplifications — paulson <lp15@cam.ac.uk> / hgweb
- removed support for experimental Pirate prover — blanchet / hgweb
#62 (Jul 25, 2021, 12:14:00 AM)
- 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)
- get rid of remote_vampire since it's hard, if possible at all, to follow Vampire's online options — blanchet / hgweb
- merged — wenzelm / hgweb
- NEWS; — wenzelm / hgweb
- proper example; — wenzelm / hgweb
- more tests; — wenzelm / hgweb
- more robust: component might be absent; — wenzelm / hgweb
- clarified global state: allow to deactivate main plugin; — wenzelm / hgweb
- more robust (again): allow to deactivate main plugin; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- more complete dockables; — wenzelm / hgweb
- more robust (see 4d91b6d5d49c); — wenzelm / hgweb
- clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- avoid non-standard encoding; — wenzelm / hgweb
- proper cross-platform build: jdk component is required for ISABELLE_SETUP_CLASSPATH in other_isabelle; — wenzelm / hgweb
- more robust classpath: skip empty entries; — wenzelm / hgweb
- more robust: avoid duplicate classpath entries; — wenzelm / hgweb
- 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 - more robust; — wenzelm / hgweb
- more portable: avoid Windows CRLF in classpath output; — wenzelm / hgweb
- proper lines (amending 59b6f0462086); — wenzelm / hgweb
- more systematic treatment of encodings; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- extended the 'corec' format slightly — blanchet / hgweb
- prefer 'xxx' to 'xxx.yyy' to 'xxx(2)' in Sledgehammer, to some extent — blanchet / hgweb
- tuning — blanchet / hgweb
- rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option — blanchet / hgweb
- correctly translate constructor argument in 'primrec' — blanchet / hgweb
- simplified a few proofs — paulson <lp15@cam.ac.uk> / hgweb
- revisited ac28714b7478: more faithful preplaying with chained facts — blanchet / hgweb
- wait for E 2.7 before using 'ite' in HO mode — blanchet / hgweb
- added alternative E binary name — blanchet / hgweb
- parse logical operators in the right order w.r.t. backtracking — blanchet / hgweb
- improved warning — blanchet / hgweb
- adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing) — blanchet / hgweb
- operations for symbolic computation of bit operations — haftmann / hgweb
- proper local context — haftmann / hgweb
- shasum for project meta-info; — wenzelm / hgweb
- even more strict shasum (amending c9771e1b3223); — wenzelm / hgweb
- clarified Isabelle meta-info within jar; — wenzelm / hgweb
- strict shasum: this is used on input files; — wenzelm / hgweb
- clarified modules;
clarified messages;
clarified return code; — wenzelm / hgweb - support for command-line operations; — wenzelm / hgweb
- operations for all components; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- merged — wenzelm / hgweb
- rebuild component; — wenzelm / hgweb
- expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER; — wenzelm / hgweb
- support expand_platform_path, which is reminiscent of isabelle.Path.expand; — wenzelm / hgweb
- skip scalac for Java build; — wenzelm / hgweb
- support mixed Scala/Java build;
clarified scalac/javac options; — wenzelm / hgweb - clarified javac options; — wenzelm / hgweb
- clarified syntax: similar to URL; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- more compiler_deps via "requirements", notably jar list from settings;
proper Files.createDirectories; — wenzelm / hgweb - clarified component settings; — wenzelm / hgweb
- clarified shasum: sources / resources within jar; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- merged — desharna / hgweb
- fixed HOL-TPTP following f58108b7a60c — desharna / hgweb
- documented Sledgehammer option "induction_rules" — desharna / hgweb
- refactored Sledgehammer option "induction_rules" — desharna / hgweb
- promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules" — desharna / hgweb
- jenkins: add pre/post-hook results for benchmark — Fabian Huch <huch@in.tum.de> / hgweb
- remove SpecCheck; it is now part of the AFP — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
#61 (Jul 18, 2021, 12:14:00 AM)
- compile — blanchet / hgweb
- more realistic timeout: 50min CPU time; — wenzelm / hgweb
- 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 - new entry Finitely_Generated_Abelian_Groups — paulson <lp15@cam.ac.uk> / hgweb
- remove duplicate entry in metadata — Lars Hupel <lars.hupel@mytum.de> / hgweb
- more coherent dependencies — haftmann / hgweb
- fix(Regex_Equivalence) update to new SpecCheck version — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb
- operations for symbolic computation of bit operations — haftmann / hgweb
- fixed Proof_Strategy_Language following Isabelle/f58108b7a60c — desharna / hgweb
- SpecCheck now without _ (Regex_Equivalence is still broken) — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
#60 (Jul 11, 2021, 12:14:00 AM)
- merged — desharna / hgweb
- added documentation for changes to Sledgehammer option "lam_trans" — desharna / hgweb
- jenkins: pre/post-hook results — Fabian Huch <huch@in.tum.de> / hgweb
- merged — desharna / hgweb
- added opaque_combs and renamed hide_lams to opaque_lifting — desharna / hgweb
- more robust treatment of empty string; — wenzelm / hgweb
- invoke Scala compiler from Java, without external process;
tuned messages; — wenzelm / hgweb - clarified version: Apple now counts like 11, 12, ...; — wenzelm / hgweb
- Imported lots of material from Stirling_Formula/Gamma_Asymptotics — paulson <lp15@cam.ac.uk> / hgweb
#60 (Jul 11, 2021, 12:14:00 AM)
- T1 fontenc for new entries — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- sitegen — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- update hide_lams -> opaque_lifting — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- merged from afp2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- website for SpecCheck — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry SpecCheck — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata and sitegen for MiniSail — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: MiniSail — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Public Announcement Logic — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry "Public Announcement Logic"
(and sorted ROOTS + removed duplicate entries in ROOTS) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb - fixed a messy reference — paulson <lp15@cam.ac.uk> / hgweb
- Van_der_Waerden website — paulson <lp15@cam.ac.uk> / hgweb
- new entry Van_der_Waerden — paulson <lp15@cam.ac.uk> / hgweb
- New entry IMP_Compiler — nipkow / hgweb
- Removal of unintended files — Susannah Mansky <susannahej@gmail.com> / hgweb
- Hidden.thy to Isar — Susannah Mansky <susannahej@gmail.com> / hgweb
- merged — desharna / hgweb
- renamed hide_lams opaque_lifting — desharna / hgweb
- merged — Fabian Huch <huch@in.tum.de> / hgweb
- jenkins: pre/post-hook results — Fabian Huch <huch@in.tum.de> / hgweb
- changed to opaque_lifiting as suggested by Isabelle/Jenkins — yonoteam <jonjulian23@gmail.com> / hgweb
- changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins — yonoteam <jonjulian23@gmail.com> / hgweb
- Added missing Public_Announcement_Logic to ROOTS file — Manuel Eberl <eberlm@in.tum.de> / hgweb
- More Support on Clean Syntax, Basic Lens Support, New Examples. — Burkhart Wolff <wolff@lri.fr> / hgweb
- 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)
- merged — paulson / hgweb
- arg for the nonstandard complex numbers — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- converting arg to Arg — paulson <lp15@cam.ac.uk> / hgweb
- just a bit of tidying up — paulson <lp15@cam.ac.uk> / hgweb
- create jar in pure Java; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified order; — wenzelm / hgweb
- proper treatment of leading zero; — wenzelm / hgweb
- support for jar resources; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- support for Isabelle/Scala in pure Java; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified directories; — wenzelm / hgweb
- clarified modules and signatures; — wenzelm / hgweb
- back to scala-2.13.5: avoid problems with history in scala REPL; — wenzelm / hgweb
- tuned imports; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified Isabelle/Java/Scala project setup; — wenzelm / hgweb
- support for Isabelle setup in pure Java; — wenzelm / hgweb
- tuned: prefer Java interfaces; — wenzelm / hgweb
- clarified package: towards stand-alone setup; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more direct java.home, according to current jdk directory layout; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified modules;
avoid initial use of _settings during init; — wenzelm / hgweb - tuned: prefer Java interfaces; — wenzelm / hgweb
- tuned: prefer Java interfaces; — wenzelm / hgweb
- clarified signature: prefer Java interfaces; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- proper usage; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified modules (again): services require full Isabelle/Scala environment; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- updated to scala-2.13.6, with scala-xml 1.3.0 ~> 2.0.0; — wenzelm / hgweb
- clarified environment (amending 9444489766a1); — wenzelm / hgweb
- merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- move code setup from Cardinality to separate theory — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- A few useful lemmas about derivatives, colinearity and other topics — paulson <lp15@cam.ac.uk> / hgweb
#59 (Jul 4, 2021, 12:14:00 AM)
- arg -> Arg: the last holdout — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- arg -> Arg — paulson <lp15@cam.ac.uk> / hgweb
- Add entry public announcement logic — Asta Halkjær From <andro.from@gmail.com> / hgweb
- merged — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- adapt to changes in HOL-Library.Cardinality — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- Added Approximation_Algorithm for Center_Selection — nipkow / hgweb
#58 (Jun 27, 2021, 12:14:00 AM)
- proper Font_Subst.cache for paintScreenLineRange; — wenzelm / hgweb
- more predictable result, avoid slightly odd "lastSubstFont" by jEdit; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- discontinue i21of4 (old Apple hardware); — wenzelm / hgweb
- avoid deprecated operation; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- support for jEdit font substitution; — wenzelm / hgweb
- more ambitious use of AttributedString (despite be825a69fc67, which was for much older Java);
more direct TextAttribute.RUN_DIRECTION_LTR (see also ce22e5c3d4ce); — wenzelm / hgweb - updated to flatlaf-1.2; — wenzelm / hgweb
- proper directories after reinstallation of lxbroy10; — wenzelm / hgweb
- more visual emphasis on node status; — wenzelm / hgweb
- more word cleanup — haftmann / hgweb
- merged — haftmann / hgweb
- more default simp rules — haftmann / hgweb
- some word streamlining — haftmann / hgweb
- avoid legacy domain informatik.tu-muenchen.de; — wenzelm / hgweb
#58 (Jun 27, 2021, 12:14:00 AM)
- proved conditional completeness of compilation — desharna / hgweb
- fixed typos — nipkow / hgweb
- more word cleanup — haftmann / hgweb
- more default simp rules — haftmann / hgweb
- some word streamlining — haftmann / hgweb
- made consistent again — haftmann / hgweb
- Fixed entry name for theories in sub-directory — Fabian Huch <huch@in.tum.de> / hgweb
- 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)
- tuned --- following hints by IntelliJ; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned signature (see 2d6a489adb01); — wenzelm / hgweb
- added support for TFX's and THF's $ite to Sledgehammer — desharna / hgweb
- tuned Mirabelle documentation — desharna / hgweb
- shortened long lines — desharna / hgweb
- fixed typos — desharna / hgweb
- updated Mirabelle documentation — desharna / hgweb
- changed Mirabelle's filter to use short theory names — desharna / hgweb
- more lemmas — haftmann / hgweb
#57 (Jun 20, 2021, 12:14:00 AM)
- Relational_Disjoint_Set_Forests: updated metadata to reflect added theory — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- Relational_Disjoint_Set_Forests: add theory More_Disjoint_Set_Forests — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- lemma grooming — haftmann / hgweb
- no duplicates of shift operations — haftmann / hgweb
- merge Jinja/Isar work — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- updated change history for Interpreter_Optimization — desharna / hgweb
- merged — paulson / hgweb
- updated, replacing axiomatizations by proper locales — paulson <lp15@cam.ac.uk> / hgweb
- added basic blocks — desharna / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Merge from default, esp JinjaDCI — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
- Updating Jinja from apply-style to Isar-style — Susannah Mansky <susannahej@gmail.com> / hgweb
#56 (Jun 13, 2021, 12:14:59 AM)
- added support for unbounded max calls to Mirabelle — desharna / hgweb
- added warnings when defining unamed or redefining Mirabelle action — desharna / hgweb
- tuned whitespace; — wenzelm / hgweb
- tuned Mirabelle — desharna / hgweb
- merged — desharna / hgweb
- refactored Mirabelle to produce output in real time — desharna / hgweb
- global interpretation into nested targets — haftmann / hgweb
- more succint interfaces — haftmann / hgweb
- merged — wenzelm / hgweb
- tuned messages; — wenzelm / hgweb
- NEWS; — wenzelm / hgweb
- proper profiling within command execution: messages require PIDE id; — wenzelm / hgweb
- more systematic treatment of profiling mode; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- prefer less intrusive tracing message; — wenzelm / hgweb
- clarified documentation: tracing messages are not shown here; — wenzelm / hgweb
- add missing file; — wenzelm / hgweb
- more formal ML profiling messages; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- Lukas Steven's more general fold foctions for maps — nipkow / hgweb
- More general fold function for maps — nipkow / hgweb
- follow Phabricator update 2021 Week 23; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more formal theory and session names;
tuned whitespace; — wenzelm / hgweb - proper NEWS after Isabelle2021; — wenzelm / hgweb
- updated descriptions; — wenzelm / hgweb
- 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 - tuned; — wenzelm / hgweb
- more robust within session "HOL"; — wenzelm / hgweb
- merged — wenzelm / hgweb
- suppress theories from other sessions, unless explicitly specified via mirabelle_theories; — wenzelm / hgweb
- clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT); — wenzelm / hgweb
- refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more uniform schedule_theories, notably for "present" and "commit" phase after loading; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- moved more legacy to AFP — haftmann / hgweb
#56 (Jun 13, 2021, 12:14:59 AM)
- Fix typo in date — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Lukas Steven's changes for his fold updates — nipkow / hgweb
- moved more legacy to AFP — haftmann / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- suppress site-gen warning — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- exclude etc/ in afp_check_roots — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- strip trailing whitespace; make full URL — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update usage instrucions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- 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 - sitegen for Lifting_the_Exponent — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Lifting_the_Exponent — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
#55 (Jun 6, 2021, 12:14:00 AM)
- clarified modules; — wenzelm / hgweb
- 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
- tuned; — wenzelm / hgweb
- more thorough update of required files (amending 1529c3eb6bac); — wenzelm / hgweb
- clarified examples; — wenzelm / hgweb
- tuned proofs; — wenzelm / hgweb
- misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a); — wenzelm / hgweb
- tuned --- reduced source complexity; — wenzelm / hgweb
- proper usage (amending f7ea394490f5); — wenzelm / hgweb
- merged, resolving minor conflict; — wenzelm / hgweb
- allow build session setup, e.g. for protocol handlers; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- tuned --- potentially more robust (e.g. session.phase_changed vs. isabelle_process.terminated); — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- removed pointless option (see 3d0952893db8); — wenzelm / hgweb
- tuned --- avoid redundant future tasks from already loaded theories; — wenzelm / hgweb
- no comment --- topological order appears to be fine since 04-Mar-2013; — wenzelm / hgweb
- more predictable sequential presentation (2f9877db82a1), without somewhat pointless result_ord (e7fab0b5dbe7); — wenzelm / hgweb
- moved stride option from sledgehammer action to main mirabelle — desharna / hgweb
- merged — paulson / hgweb
- new lemmas mostly about paths — paulson <lp15@cam.ac.uk> / hgweb
- lexorders the locale way — haftmann / hgweb
- more accurate export morphism enables proper instantiation by interpretation — haftmann / hgweb
#55 (Jun 6, 2021, 12:14:00 AM)
- more specific export_files: omit recent additions ("document", "PIDE", etc.); — wenzelm / hgweb
- grouped lemmas — haftmann / hgweb
- bundles for traditional infix syntax — haftmann / hgweb
#54 (May 30, 2021, 12:14:00 AM)
- merged — paulson / hgweb
- some new and/or varient results about images — paulson <lp15@cam.ac.uk> / hgweb
- nicer statement of Liouville_theorem — paulson <lp15@cam.ac.uk> / hgweb
- more lemmas — haftmann / hgweb
- max word moved to Word_Lib in AFP — haftmann / hgweb
- more robust syntax; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- clarified document export names; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac; — wenzelm / hgweb
- compose Latex text as XML, output exported YXML in Isabelle/Scala; — wenzelm / hgweb
- more direct index_entry: no positions required -- text is eventually moved to .ind file; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle"); — wenzelm / hgweb
- tuned message, e.g. for Pure bootstrap; — wenzelm / hgweb
- proper signature export (amending b50f8cc8c08e); — wenzelm / hgweb
- syslog option for "isabelle build"; — wenzelm / hgweb
- further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea); — wenzelm / hgweb
- merged — wenzelm / hgweb
- NEWS; — wenzelm / hgweb
- clarified index, more like formal @{element_ref}; — wenzelm / hgweb
- clarified treatment of type constructors; — wenzelm / hgweb
- misc tuning and clarification; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified context; — wenzelm / hgweb
- more uniform document antiquotations for ML: consolidate former setup for manuals; — wenzelm / hgweb
- clarified names; — wenzelm / hgweb
- clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature: avoid dispatch via name; — wenzelm / hgweb
- clarified, e.g. type variables; — wenzelm / hgweb
- tuned index; — wenzelm / hgweb
- more ambitious default for index "is like"; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- support for index entries; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified old document build; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been removed already in 435fb018e8ee; — wenzelm / hgweb
- prefer standard document_build=lualatex --- no impact of "sedindex" in prepare_document; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- proper Unix lines; — wenzelm / hgweb
- prefer explicit option document_bibliography (actually ignored by build script); — wenzelm / hgweb
- explicit option document_bibliography; — wenzelm / hgweb
- proper bibliography; — wenzelm / hgweb
- discontinued obsolete "isabelle latex"; — wenzelm / hgweb
- 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 - default document_build (lualatex); — wenzelm / hgweb
- more robust: allow \printindex within the document; — wenzelm / hgweb
- clarified bash scripts, with public interfaces for user-defined Document_Build.Engine; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- option document_preprocessor; — wenzelm / hgweb
- show symbols in Isabelle/ML instead of perl; — wenzelm / hgweb
- more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; — wenzelm / hgweb
- tuned --- more robust; — wenzelm / hgweb
- discontinued somewhat pointless "fixbookmarks": default output works sufficiently well; — wenzelm / hgweb
- more uniform bibtex error, without using perl (see 4710dd5093a3); — wenzelm / hgweb
- proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error); — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified command-line options; — wenzelm / hgweb
- obsolete (see 5a3a2a52648d); — wenzelm / hgweb
- redundant: copy produced from session document_files; — wenzelm / hgweb
- clarified treatment of Isabelle .sty files; — wenzelm / hgweb
- option document_logo; — wenzelm / hgweb
- proper options; — wenzelm / hgweb
- option document_build refers to build engine in Isabelle/Scala;
pdflatex is back as legacy build engine, e.g. for published proceedings; — wenzelm / hgweb - redundant: tmp_dir is purged anyway; — wenzelm / hgweb
- misc tuning and clarification; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- tuned --- clarified corner cases; — wenzelm / hgweb
- more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases; — wenzelm / hgweb
- clarified signature -- avoid odd warning about scala/bug#6675; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- proper syntax of Scala 3; — wenzelm / hgweb
- enforce syntax of Scala 3; — wenzelm / hgweb
#54 (May 30, 2021, 12:14:00 AM)
- complement reduced to mere abbreviation — haftmann / hgweb
- extracted more legacy abbreviations — haftmann / hgweb
- max word moved to Word_Lib in AFP — haftmann / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update website — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fix links — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Restore deleted theorem from Szpilrajn — Lukas Stevens <mail@lukas-stevens.de> / hgweb
- tuned presentation — haftmann / hgweb
- adapted to devel — nipkow / hgweb
- adjusted to changes in distribution — haftmann / hgweb
- adjust Combinatorics_Words to isabelle@493b1ae188da — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- make AFP ROOTS globally available for component — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merged — nipkow / hgweb
- New entries Combinatorics_Words* — nipkow / hgweb
- adjusted to change in distribution — haftmann / hgweb
- adapted to Isabelle/466fae6bf22e; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- Remove comment about missing refinement — n.muendler <n.muendler@tum.de> / hgweb
- continued uglification, but also fixed some dodgy proofs — paulson <lp15@cam.ac.uk> / hgweb
- fixed some broken / looping / fragile proofs — paulson <lp15@cam.ac.uk> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- simplify usage instructions more — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- sitegen for Padic_Ints — Manuel Eberl <eberlm@in.tum.de> / hgweb
- new entry: Padic_Ints — Manuel Eberl <eberlm@in.tum.de> / hgweb
- update affiliation — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- New entry: Regressioon_Test_Selection — nipkow / hgweb
- metadata for Metalogic_ProofChecker — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Metalogic_ProofChecker — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata for GaleStewart_Games — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry GaleStewart_Games — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- fixed the ROOT file ofr BenOr_Kozen_Reif — paulson <lp15@cam.ac.uk> / hgweb
- webpage for BenOr_Kozen_Reif — paulson <lp15@cam.ac.uk> / hgweb
- new entry BenOr_Kozen_Reif — paulson <lp15@cam.ac.uk> / hgweb
- Slight tidying to shorten too-long lines — paulson <lp15@cam.ac.uk> / hgweb
- added a necessary acknowledgment (ERC) — paulson <lp15@cam.ac.uk> / hgweb
- New entry Progress_Tracking — nipkow / hgweb
- Revisions by Wenda to eliminate the locale comp_affine_scheme — paulson <lp15@cam.ac.uk> / hgweb
- renamed a lemma — paulson <lp15@cam.ac.uk> / hgweb
- 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
- consolidated metadata of Anthony Bordg, metadata for new Grothendieck entry + sitegen — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry: Grothendieck_Schemes — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- metadata for IFC_Tracking — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry IFC_Tracking — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- merged — wenzelm / hgweb
- adapted to Isabelle/ef1a18e20ace; — wenzelm / hgweb
- recover some patches after years of continuously changing Isabelle LaTeX output; — wenzelm / hgweb
- prefer document_preprocessor over document_build; — wenzelm / hgweb
- prefer document_logo instead of document_build script; — wenzelm / hgweb
- proper options; — wenzelm / hgweb
#53 (May 23, 2021, 12:14:00 AM)
- things need to be ugly — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- sorted as an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
- mere abbreviation for logical alias — haftmann / hgweb
- avoid unexpected output+behaviour when CDPATH is set — kleing / hgweb
- recover some Linux test, using old macbroy2 as i21of4 (Ubuntu 20.04); — wenzelm / hgweb
- avoid perl; — wenzelm / hgweb
- tuned signature --- following hints by IntelliJ IDEA; — wenzelm / hgweb
- ignore session build timeout, notably in AFP; — wenzelm / hgweb
- check timeout_ignored as in ML, before applying timeout_scale; — wenzelm / hgweb
- merged — wenzelm / hgweb
- proper build of required session images vs. build with Mirabelle presentation; — wenzelm / hgweb
- reactive "sledgehammer"; — wenzelm / hgweb
- reactive "sledgehammer_filter": statically correct, but untested (no proof_file); — wenzelm / hgweb
- clarified command-line; — wenzelm / hgweb
- clarified signature;
supporess empty results; — wenzelm / hgweb - clarified signature; — wenzelm / hgweb
- clarified log content; — wenzelm / hgweb
- reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- unused (see 8ffc607c345d); — wenzelm / hgweb
- clarified signature: provide access to previous state; — wenzelm / hgweb
- clarified signature (see Scala version); — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- avoid duplicate loading of ML file; — wenzelm / hgweb
#53 (May 23, 2021, 12:14:00 AM)
- PATCH to Auto2 (for sorted) by Bohua, pending a permanent generalisation of "properties" — paulson <lp15@cam.ac.uk> / hgweb
- fixed two more "sorted" errors — paulson <lp15@cam.ac.uk> / hgweb
- fixed two "sorted" issues — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- changes for "sorted" as an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
- mere abbreviation for logical alias — haftmann / hgweb
- eliminated odd clone (see Isabelle/caa5a257d3ed); — wenzelm / hgweb
#52 (May 16, 2021, 12:14:00 AM)
- strict_sorted now an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
- explicit type class operations for type-specific implementations — haftmann / hgweb
- obsolete — haftmann / hgweb
- added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran — desharna / hgweb
- merged — nipkow / hgweb
- generalized type — nipkow / hgweb
- basic setup of Isabelle setup tool --- pure Java, no dependencies; — wenzelm / hgweb
- merged — wenzelm / hgweb
- guess package more directly; — wenzelm / hgweb
- merged — paulson / hgweb
- Just one lemma — paulson <lp15@cam.ac.uk> / hgweb
- proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64; — wenzelm / hgweb
- clarified platforms; — wenzelm / hgweb
- merged — wenzelm / hgweb
- proper jEdit.props (amending ff716ecb0805); — wenzelm / hgweb
- update to gmp-6.2.1, with support for arm64-darwin; — wenzelm / hgweb
- clarified platforms; — wenzelm / hgweb
- clarified options: implicitly support both x86_64 and arm64; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- centralized more lemmas — haftmann / hgweb
- avoid Fun.swap — haftmann / hgweb
- guide is out of focus — haftmann / hgweb
- proper build for fresh target directory (amending d9823224fcfe); — wenzelm / hgweb
- put more resources into jedit_build component; — wenzelm / hgweb
- more brackets (see f6b453449cc6); — wenzelm / hgweb
- more brackets; — wenzelm / hgweb
- proper settings variable, amending 6e85281177df; — wenzelm / hgweb
- merged — wenzelm / hgweb
- tuned proofs --- avoid z3, which is absent on arm64-linux; — wenzelm / hgweb
- proper condition: z3 could be absent, e.g. on arm64-linux; — wenzelm / hgweb
- build auxiliary jEdit component in Isabelle/Scala;
clarified directory layout; — wenzelm / hgweb - separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597); — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- more elementary swap — haftmann / hgweb
#52 (May 16, 2021, 12:14:00 AM)
- strict_sorted now an abbreviation — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- deleted needless material — paulson <lp15@cam.ac.uk> / hgweb
- explicit type class operations for type-specific implementations — haftmann / hgweb
- next step to phase out ancient numerals — haftmann / hgweb
- more small simplifications — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- fixed some latex; tried the alternative definition of Ramsey — paulson <lp15@cam.ac.uk> / hgweb
- Trying out Ramsey_eq for simpler proofs — paulson <lp15@cam.ac.uk> / hgweb
- more tiny tweaks — paulson <lp15@cam.ac.uk> / hgweb
- centralized more lemmas — haftmann / hgweb
- avoid Fun.swap — haftmann / hgweb
- guide is out of focus — haftmann / hgweb
- Relational_Minimum_Spanning_Trees: refactoring Boruvka.thy — Walter Guttmann <walter.guttmann@canterbury.ac.nz> / hgweb
- more elementary swap — haftmann / hgweb
#49 (Apr 25, 2021, 12:14:00 AM)
#49 (Apr 25, 2021, 12:14:00 AM)
#47 (Apr 21, 2021, 10:29:10 AM)
- proper use of antiquotations; — wenzelm / hgweb
- more documentation on "Conversions"; — wenzelm / hgweb
- tuned — nipkow / hgweb
- updated example; — wenzelm / hgweb
- clarified options (again); — wenzelm / hgweb
- more options: update ISABELLE_IDENTIFIER; — wenzelm / hgweb
- clarified conditional ML; — wenzelm / hgweb
- support for conditional ML text; — wenzelm / hgweb
- updated example; — wenzelm / hgweb
- clarified options; — wenzelm / hgweb
- proper context variable handling when stripping leadings quantifiers from test goals — haftmann / hgweb
- proper etc/ISABELLE_ID from archive (amending 4cba4e250c28); — wenzelm / hgweb
- eliminated perl: prefer elementary GNU printenv; — wenzelm / hgweb
- more robust bootstrap of components; — wenzelm / hgweb
- more self-contained support for macOS; — wenzelm / hgweb
- misc tuning and clarification; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- support for base64 via Isabelle/Scala/ML; — wenzelm / hgweb
- compile; — wenzelm / hgweb
- clarified signature: avoid overlap of String vs. Bytes (both are CharSequence); — wenzelm / hgweb
- clarified signature (again); — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- clarified signature: more structured arguments, notably for remote provers; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature: avoid tmp file; — wenzelm / hgweb
- clarified signature for Scala functions; — wenzelm / hgweb
- clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9); — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified cache; — wenzelm / hgweb
- clarified signature: Bytes extends CharSequence already (see d201996f72a8); — wenzelm / hgweb
- clarified exceptions; — wenzelm / hgweb
- more uniform use of Byte_Message;
support protocol_message with multiple chunks; — wenzelm / hgweb - tuned signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- more robust treatment of empty markup: it allows to produce formal chunks; — wenzelm / hgweb
- collected combinatorial material — haftmann / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more documentation; — wenzelm / hgweb
- proper treatment of nested antiquotations;
clarified signature; — wenzelm / hgweb - support for ML special forms: modified evaluation similar to Scheme; — wenzelm / hgweb
- clarified signature: more detailed token positions for antiquotations; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- confluent preprocessing for floats in presence of target language numerals — haftmann / hgweb
- subclass relation — haftmann / hgweb
- some tinkering with npm versions; — wenzelm / hgweb
- some tinkering with npm versions; — wenzelm / hgweb
- back to post-release mode; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- auto-update due to "isabelle build_vscode"; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned --- following hints by IntelliJ IDEA; — wenzelm / hgweb
- fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes) — Manuel Eberl <eberlm@in.tum.de> / hgweb
- simplified definition — haftmann / hgweb
- new lemmas — haftmann / hgweb
- discontinue old Ubuntu 18.04 LTS, e.g. it cannot build documentation "prog-prove"; — wenzelm / hgweb
- following recent Phabricator update, after 2021 Week 13 (Late March); — wenzelm / hgweb
- merged — paulson / hgweb
- Cosmetic: no !! in the lemma statement — paulson <lp15@cam.ac.uk> / hgweb
- clarified README;
avoid odd patching of sources; — wenzelm / hgweb - more standard header, with utf-8 encoding; — wenzelm / hgweb
- clarified HTML template (see also 04cb7e02ca38): avoid odd patching of sources; — wenzelm / hgweb
- merged — nipkow / hgweb
- new automatic order prover: stateless, complete, verified — nipkow / hgweb
- clarified signature; — wenzelm / hgweb
- clarified: follow "isabelle version -t"; — wenzelm / hgweb
- further clarification of Isabelle distribution identification -- avoid odd patching of sources; — wenzelm / hgweb
- tuned signature -- more explicit types; — wenzelm / hgweb
- more robust and uniform ISABELLE_TAGS; — wenzelm / hgweb
- clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos; — wenzelm / hgweb
- simplified release status (again), in contrast to a43898f76ae9; — wenzelm / hgweb
- more uniform HTTP resources; — wenzelm / hgweb
- clarified (again): local tip could be actually more recent; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified name; — wenzelm / hgweb
- more systematic java_library: avoid empty entries, declaration order as for other bash functions; — wenzelm / hgweb
- support sequential LaTeX jobs: more robust when TeX installation is self-installing packages etc.; — wenzelm / hgweb
- updated to latest latex due to new mechanism for dealing with bold ccfonts — nipkow / hgweb
- removal of needless hypothesis in hd_rev and last_rev — paulson <lp15@cam.ac.uk> / hgweb
#47 (Apr 21, 2021, 10:29:10 AM)
- more realistic timeout; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
- Tweaks — Asta Halkjær From <andro.from@gmail.com> / hgweb
- adapted to Isabelle/a2c589d5e1e4; — wenzelm / hgweb
- Merge — paulson <lp15@cam.ac.uk> / hgweb
- tweak — paulson <lp15@cam.ac.uk> / hgweb
- simplified proof — nipkow / hgweb
- sshiftr/bl lemmas by Florian Märkl — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- proof simplification — paulson <lp15@cam.ac.uk> / hgweb
- cosmetic tweaks to proofs — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- minor stylistic changes — paulson <lp15@cam.ac.uk> / hgweb
- Add completeness of modal logics T, KB, K4, S4 and S5 — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Stylistic tweaks, which I hope are improvements :-) — paulson <lp15@cam.ac.uk> / hgweb
- updated paper references — traytel / hgweb
- merge — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- increased timeout — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- collected combinatorial material — haftmann / hgweb
- Update root.tex — Asta Halkjær From <andro.from@gmail.com> / hgweb
- Cut out Fitting's consistency properties — Asta Halkjær From <andro.from@gmail.com> / hgweb
- fixed proof — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- clarified message, following Isabelle/a7aabdf889b7; — wenzelm / hgweb
- confluent preprocessing for floats in presence of target language numerals — haftmann / hgweb
- subclass relation — haftmann / hgweb
- adapted to isabelle-dev/56db8559eadb — Manuel Eberl <eberlm@in.tum.de> / hgweb
- simplified definition — haftmann / hgweb
- new lemmas — haftmann / hgweb
- probable fix suggested by Cornelius for the changes in the vicinity of 2cd23d587db9 — nipkow / hgweb
- Fixes due to new order prover — nipkow / hgweb
- another broken proof — paulson <lp15@cam.ac.uk> / hgweb
- Fixed and simplified some failing proofs — paulson <lp15@cam.ac.uk> / hgweb
- Writing less_sets as an infix — paulson <lp15@cam.ac.uk> / hgweb
- avoid symblinks --- make it work on Windows; — wenzelm / hgweb
- Fixed some looping proofs (though why they were looping isn't clear) — paulson <lp15@cam.ac.uk> / hgweb
- Fixed a failing proof — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- fixes for new hd_rev and last_rev — paulson <lp15@cam.ac.uk> / hgweb
#42 (Apr 4, 2021, 12:14:00 AM)
- more robust; — wenzelm / hgweb
- clarified message; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- proper export; — wenzelm / hgweb
- more options: build is part of default setup; — wenzelm / hgweb
- misc tuning and clarification; — wenzelm / hgweb
- more options; — wenzelm / hgweb
- proper Admin script, outside the settings environment; — wenzelm / hgweb
- tuned whitespace; — wenzelm / hgweb
#42 (Apr 4, 2021, 12:14:00 AM)
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Infix notation for the less_sets relation — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- simplified a few proofs — paulson <lp15@cam.ac.uk> / hgweb
- sitegen and metadata for Constructive_Cryptography_CM — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- new entry Constructive_Cryptography_CM — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
#41 (Mar 28, 2021, 12:14:00 AM)
- tuned; — wenzelm / hgweb
- clarified; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- more accurate settings after update of current version; — wenzelm / hgweb
- clarified messages; — wenzelm / hgweb
- more robust: lest hg work out remote tip;
more options; — wenzelm / hgweb - more options; — wenzelm / hgweb
- clarified treatment of multiple versions: last one counts;
more options; — wenzelm / hgweb - more robust; — wenzelm / hgweb
- more robust: explicit repository root; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- more convenient repository setup; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more robust invocation of hg; — wenzelm / hgweb
- more robust: idempotent; — wenzelm / hgweb
- more robust invocation of hg; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified output;
more options; — wenzelm / hgweb - support repository archives (without full .hg directory); — wenzelm / hgweb
- more robust invocation of hg; — wenzelm / hgweb
- 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
- dedicated session for combinatorial material — haftmann / hgweb
- support for Java Chromium Embedded Framework (JCEF): still somewhat fragile; — wenzelm / hgweb
- enforce full build; — wenzelm / hgweb
- turn LaTeX warning into error, for the sake of isabelle.sty/bbbfont; — wenzelm / hgweb
- discontinue fragile check in LaTeX, e.g. problems with toc entries; — wenzelm / hgweb
- merged — paulson / hgweb
- merged — paulson / hgweb
- type class relaxation — paulson <lp15@cam.ac.uk> / hgweb
- more NEWS; — wenzelm / hgweb
- clarified group (but hard to tell); — wenzelm / hgweb
- more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd;
corresponding symbols and latex macros; — wenzelm / hgweb - more lemmas — haftmann / hgweb
- clarified package name (actually both pxfonts and txfonts exist and have this font); — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- prefer isabelle bbbfont; — wenzelm / hgweb
- enforce full build; — wenzelm / hgweb
- clarified symbol names, notably relevant for Z_Notation; — wenzelm / hgweb
- update README (actually after update of component); — wenzelm / hgweb
- high-quality blackboard-bold fonts from "txmia" (package "txfonts"); — wenzelm / hgweb
#41 (Mar 28, 2021, 12:14:00 AM)
- more robust invocation of hg; — wenzelm / hgweb
- Update tile to match metadata — Lukas Stevens <mail@lukas-stevens.de> / hgweb
- Extend entry Szpilrajn — Lukas Stevens <mail@lukas-stevens.de> / hgweb
- dedicated session for combinatorial material — haftmann / hgweb
- more lemmas — haftmann / hgweb
#40 (Mar 21, 2021, 12:14:00 AM)
- publish component; — wenzelm / hgweb
- further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster; — wenzelm / hgweb
- clarified \<Zcomp> (small) vs. \<Zsemi> (big); — wenzelm / hgweb
- more CONTRIBUTORS; — wenzelm / hgweb
- 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 - more accurate glyphs 0x25C1 / 0x25B7, based on 0x2A64 / 0x2A65 minus the "minus"; — wenzelm / hgweb
- clarified order for GUI panel; — wenzelm / hgweb
- prefer more direct interpretation — haftmann / hgweb
- more Z_Notation symbols, as proposed by Simon Foster; — wenzelm / hgweb
- more accurate spacing, according to results seen in isar-ref (Appendix B), using 12pt or 10pt; — wenzelm / hgweb
- clarified order for presentation in isar-ref (Appendix B); — wenzelm / hgweb
- prefer explicit \<Zproject> (with its own Unicode codepoint); — wenzelm / hgweb
- 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 - tuned message; — wenzelm / hgweb
- proper directory of settings file;
tuned; — wenzelm / hgweb - tuned lemma — nipkow / hgweb
- added lemma — nipkow / hgweb
- tuned signature; — wenzelm / hgweb
- tuned signature (again); — wenzelm / hgweb
- tuned --- following hints by IntelliJ; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- proper shell quote; — wenzelm / hgweb
- removed spurious references to perl / libwww-perl; — wenzelm / hgweb
- 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 - clarified signature: refer to file name instead of file content; — wenzelm / hgweb
- compile; — wenzelm / hgweb
- clarified signature: more explicit types; — wenzelm / hgweb
- support for SystemOnTPTP.run_system, with strict error following scripts/remote_atp; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- elapsed time to download content (and for the server to provide content); — wenzelm / hgweb
- more direct elapsed run_time via bash_process wrapper (via Scala and C); — wenzelm / hgweb
#40 (Mar 21, 2021, 12:14:00 AM)
- neater proof — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- Removal of an unused theorem. Plus lots of white space — paulson <lp15@cam.ac.uk> / hgweb
- switch new entries' documents to T1 encoding — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- merge from afp-2021 — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- corrected metadata (use acute's in names of J. Divasón and René T.) — Rene Thiemann <rene.thiemann@uibk.ac.at> / hgweb
- sitegen for Modular_arithmetic_LLL_and_HNF_algorithms — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- metadata for Modular_arithmetic_LLL_and_HNF_algorithms — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- new entry Modular_arithmetic_LLL_and_HNF_algorithms — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- a slight streamlining — paulson <lp15@cam.ac.uk> / hgweb
- Hermite_Lindemann website — paulson <lp15@cam.ac.uk> / hgweb
- new entry Hermite_Lindemann — paulson <lp15@cam.ac.uk> / hgweb
- cosmetic changes — paulson <lp15@cam.ac.uk> / hgweb
- Projective_Measurements website — paulson <lp15@cam.ac.uk> / hgweb
- Projective_Measurements with files — paulson <lp15@cam.ac.uk> / hgweb
- new entry Projective_Measurements — paulson <lp15@cam.ac.uk> / hgweb
- add Andreas Lochbihler as editor — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- New entry: Mereology — nipkow / hgweb
- New entry Sunflowers — nipkow / hgweb
- refactored and added lemma state_behaves_forward_to_backward — desharna / hgweb
#39 (Mar 14, 2021, 12:14:00 AM)
- merged — wenzelm / hgweb
- use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages; — wenzelm / hgweb
- clarified signature: let Sledgehammer handle SystemOnTPTP comments; — wenzelm / hgweb
- clarified signature: url may change dynamically and is part of result; — wenzelm / hgweb
- clarified error; — wenzelm / hgweb
- support timeout, similar to perl LWP::UserAgent; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML; — wenzelm / hgweb
- support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl); — wenzelm / hgweb
- clarified HTTP.Content: support encoding;
more realistic HTTP.Client operations; — wenzelm / hgweb - clarified signature: more explicit HTTP operations; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified components; — wenzelm / hgweb
- avoid name clash — haftmann / hgweb
- lemma — haftmann / hgweb
- tuned; — wenzelm / hgweb
- another example for lift_bnf for quotients — traytel / hgweb
- merged — wenzelm / hgweb
- proper \usepackage[T1]{fontenc}; — wenzelm / hgweb
- more robust init: avoid spilling opam artifacts; — wenzelm / hgweb
- proper type-setting of cartouches (requires T1);
\usepackage[T1]{fontenc} is default for mkroot;
\usepackage[utf8]{inputenc} is obsolete in lualatex; — wenzelm / hgweb - provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04; — wenzelm / hgweb
- more robust;
eliminated perl; — wenzelm / hgweb - removed unused latex packages; — wenzelm / hgweb
- obsolete (see 0c837beeb5e7); — wenzelm / hgweb
- proper Isabelle/Scala tool --- avoid perl; — wenzelm / hgweb
- generalized confluence-based subdistributivity theorem for quotients;
new example that triggered the generalization — traytel / hgweb - Backed out changeset 3fdb94d87e0e — desharna / hgweb
- Backed out changeset b867b436f372 — desharna / hgweb
- reduced dependencies on List_Permutation — haftmann / hgweb
- follow corresponding precedence on sets — haftmann / hgweb
- consolidated names — haftmann / hgweb
- reduced dependencies on theory List_Permutation — haftmann / hgweb
#39 (Mar 14, 2021, 12:14:00 AM)
- avoid name clash — haftmann / hgweb
- 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 - reduced dependencies on List_Permutation — haftmann / hgweb
- follow corresponding precedence on sets — haftmann / hgweb
- consolidated names — haftmann / hgweb
- reduced dependencies on theory List_Permutation — haftmann / hgweb
#38 (Mar 7, 2021, 12:14:00 AM)
- obsolete (see f3378101f555); — wenzelm / hgweb
- merged — wenzelm / hgweb
- more direct unlimited smt_timeout;
update of certificates: generated command-line options are part of input / digest; — wenzelm / hgweb - clarified smt: support Timeout.ignored and Timeout.scale_time; — wenzelm / hgweb
- clarified timeouts in Isabelle/ML; — wenzelm / hgweb
- tuned --- more elementary Time operations; — wenzelm / hgweb
- removed unused/pointless operation: Time.start is the load/init time of this Scala module; — wenzelm / hgweb
- obsolete; — wenzelm / hgweb
- clarified signature --- augment existing structure Time; — wenzelm / hgweb
- rebuild SMT certificates from scratch; — wenzelm / hgweb
- added lemmas (sublist|prefix|suffix)_list_all — desharna / hgweb
- added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While — desharna / hgweb
- added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI — desharna / hgweb
- typo — haftmann / hgweb
- merged — desharna / hgweb
- added upper bound on monomorphisation duplicate instances — desharna / hgweb
- tuned best_slices in atp_config — desharna / hgweb
- tuned exec field in atp_config — desharna / hgweb
- removed junk; — wenzelm / hgweb
- tuned proofs; — wenzelm / hgweb
- enforce full build, after significant changes in Isabelle/Scala; — wenzelm / hgweb
- clarified compiler options: show relevant warnings; — wenzelm / hgweb
- tuned --- avoid compiler warnings; — wenzelm / hgweb
- clarified signature --- fewer warnings; — wenzelm / hgweb
- clarified signature --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- more robust ordering (see also 88c96e836ed6); — wenzelm / hgweb
- proper scala.collection.immutable; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- more robust error; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- updated to scala-2.13.5 (with scala-swing_2.13-3.0.0); — wenzelm / hgweb
- slightly more efficient Term.fastype_of (only little impact in regular applications); — wenzelm / hgweb
- reduced dependencies on theory List_Permutation — haftmann / hgweb
- Merge — paulson <lp15@cam.ac.uk> / hgweb
- reverted simprule status on a new lemma — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- tiny bit of lemma hacking — paulson <lp15@cam.ac.uk> / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- avoid deprecated conversions between certain number type; — wenzelm / hgweb
- tuned --- avoid deprecated Predef.any2stringadd; — wenzelm / hgweb
- tuned --- silence odd warning; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- tuned --- fewer warnings; — wenzelm / hgweb
- clarified signature, according to Isabelle/Scala; — wenzelm / hgweb
- download more directly, via means of JVM; — wenzelm / hgweb
- download on separate thread; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.); — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- NEWS — haftmann / hgweb
- lemma diffusion — haftmann / hgweb
- more connections between mset _ = mset _ and permutations — haftmann / hgweb
- dissolve theory with duplicated name from afp — haftmann / hgweb
- more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept; — wenzelm / hgweb
- more Isabelle/ML/Scala operations; — wenzelm / hgweb
- more Isabelle/ML/Scala operations; — wenzelm / hgweb
- more Isabelle/ML/Scala operations;
clarified errors; — wenzelm / hgweb - proper src1, amending 20157c8ab3f3; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- proper File.eq, amending df49ca5da9d0; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified modules: more like ML; — wenzelm / hgweb
- obsolete; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552); — wenzelm / hgweb
- 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)
- tuned — nipkow / hgweb
- Tuned presentation of Buffon's needle — Manuel Eberl <eberlm@in.tum.de> / hgweb
- tuned — nipkow / hgweb
- reduced dependencies on theory List_Permutation — haftmann / hgweb
- tidied up messy proofs — paulson <lp15@cam.ac.uk> / hgweb
- lemma diffusion — haftmann / hgweb
- more connections between mset _ = mset _ and permutations — haftmann / hgweb
- dissolve theory with duplicated name from afp — haftmann / hgweb
#37 (Feb 28, 2021, 12:14:00 AM)
- more checks; — wenzelm / hgweb
- clarified message; — wenzelm / hgweb
- clarified message; — wenzelm / hgweb
- clarified comments; — wenzelm / hgweb
- clarified message; — wenzelm / hgweb
- improved list_neq simproc — nipkow / hgweb
- merged — haftmann / hgweb
- repaired document — haftmann / hgweb
- merged — paulson / hgweb
- merged — paulson / hgweb
- A couple of basic lemmas about arg — paulson <lp15@cam.ac.uk> / hgweb
- multiset as equivalence class of permuted lists — haftmann / hgweb
- emphasize connection to multisets — haftmann / hgweb
- proper "latest" tag, otherwise the default pull command from https://hub.docker.com/r/makarius/isabelle won't work; — wenzelm / hgweb
- more on Isabelle_System.bash; — wenzelm / hgweb
- more specific name — haftmann / hgweb
- more lemmas — haftmann / hgweb
- dropped obscure FIXME — haftmann / hgweb
- proper usage of hypotheses for zipperposition's TPTP generation — desharna / hgweb
- merged — desharna / hgweb
- tuned Mirabelle to parse option check_trivial only once — desharna / hgweb
- merged — desharna / hgweb
- merged — desharna / hgweb
- added stride option to Mirabelle — desharna / hgweb
- proper prover capabilities for zipperposition — desharna / hgweb
- NEWS; — wenzelm / hgweb
- merged — wenzelm / hgweb
- clarified uses of Isabelle_System.bash_process: more checks, fewer messages; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- more direct timing from bash_process wrapper; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature, following Isabelle/Scala; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code; — wenzelm / hgweb
- clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature, following Isabelle/Scala; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- clarified signature: process_result timing from Isabelle/Scala; — wenzelm / hgweb
- NEWS — haftmann / hgweb
- dedicated locale for preorder and abstract bdd operation — haftmann / hgweb
- get rid of traditional predicate — haftmann / hgweb
- proper treatment of process_result; — wenzelm / hgweb
- more accurate process_result in ML, corresponding to Process_Result in Scala; — wenzelm / hgweb
- clarified: proper trim_line for error; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- clarified lines (again); — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- more uniform Bash.process: always ask Isabelle/Scala; — wenzelm / hgweb
- more reactive protocol messages, e.g. for Scala.function (relevant for Bash.process); — wenzelm / hgweb
- clarified compiler options; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- removed obsolete RC tags; — wenzelm / hgweb
#37 (Feb 28, 2021, 12:14:00 AM)
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- revert accidental change — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- website update — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fix typo (Bauer -> Bayer) — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- new entry BTree — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add Windows example to use-instructions — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Isabelle app layout changed on Mac — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- Formal_Puiseux_Series website — paulson <lp15@cam.ac.uk> / hgweb
- new entry Formal_Puiseux_Series — paulson <lp15@cam.ac.uk> / hgweb
- 2021 web pages — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update with 2021 release .tar.gz's — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- add Isabelle2021 release date — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- update .tar.gz releases — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- set version to 2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- multiset as equivalence class of permuted lists — haftmann / hgweb
- emphasize connection to multisets — haftmann / hgweb
- more specific name — haftmann / hgweb
- merged — wenzelm / hgweb
- adapted to Isabelle/0110e2e2964c; — wenzelm / hgweb
- adapted to Isabelle/f0db1e4c89bc; — wenzelm / hgweb
- dedicated locale for preorder and abstract bdd operation — haftmann / hgweb
- get rid of traditional predicate — haftmann / hgweb
- more accurate process_result; — wenzelm / hgweb
- adapted to Isabelle/440546ea20e6; — wenzelm / hgweb
#36 (Feb 21, 2021, 12:14:00 AM)
- more hints; — wenzelm / hgweb
- merged — wenzelm / hgweb
- Added tag Isabelle2021 for changeset 7e2a9a8c2b85 — wenzelm / hgweb
- provide naproche-755224402e36; — wenzelm / hgweb
- provide naproche-4ad61140062f; — wenzelm / hgweb
- HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc. — Manuel Eberl <eberlm@in.tum.de> / hgweb
- tidied up a few ugly proofs — paulson <lp15@cam.ac.uk> / hgweb
- merged — wenzelm / hgweb
- provide naproche-6d0d76ce2f2a; — wenzelm / hgweb
- Added tag Isabelle2021-RC6 for changeset ed36e33a2e4b — wenzelm / hgweb
- updated to flatlaf-1.0; — wenzelm / hgweb
- tuned NEWS; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- more robust interrupt handling as in Future.forked_results (amending 64df1e514005); — wenzelm / hgweb
- more parallelism: avoid exhaustion of standard thread pool; — wenzelm / hgweb
#36 (Feb 21, 2021, 12:14:00 AM)
- follow_on changes from Complex_Geometry — paulson <lp15@cam.ac.uk> / hgweb
- merged — paulson / hgweb
- a massive simplification, thanks to sledgehammer, etc. — paulson <lp15@cam.ac.uk> / hgweb
- adapted to isabelle-dev/73253:f6bb31879698 — Manuel Eberl <eberlm@in.tum.de> / hgweb
- Buffons_Needle: tuned presentation — Manuel Eberl <eberlm@in.tum.de> / hgweb
- 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)
- merged — wenzelm / hgweb
- updated for release; — wenzelm / hgweb
- Added tag Isabelle2021-RC4 for changeset 2ab14dbc6feb — wenzelm / hgweb
- provide naproche-20210201; — wenzelm / hgweb
- clarified messages; — wenzelm / hgweb
- more parallel; — wenzelm / hgweb
- more parallel; — wenzelm / hgweb
- contributors — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- hide the internal abbreviations MR and MB — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- optimize RBT_Impl — mraszyk / hgweb
- merged — wenzelm / hgweb
- more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup); — wenzelm / hgweb
- tuned signature: more types; — wenzelm / hgweb
- clarified signature: proper order; — wenzelm / hgweb
- clarified signature: more explicit types; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified signature: no symbol markup within XML attributes; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
- bundle more libraries from scala-2.12.x, notably for Isabelle/MMT; — wenzelm / hgweb
- provide naproche-20210129; — wenzelm / hgweb
- more robust type signatures, notably for the sake of haskell-stack-trace-plugin-0.1.1.1; — wenzelm / hgweb
- tuned signature (e.g. see HTML.control_block in Isabelle/Scala); — wenzelm / hgweb
- proper Isabelle environment (amending 31fbde3baa97); — wenzelm / hgweb
- updated to jdk-15.0.2+7; — wenzelm / hgweb
- follow Phabricator update 2021 Week 4; — wenzelm / hgweb
- more NEWS; — wenzelm / hgweb
- 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 - more generic Isabelle_app; — wenzelm / hgweb
- prefer dynamic linking: platform is always x86_64 (see 373dcdd363dc); — wenzelm / hgweb
- more robust; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- provide jdk-11.0.10+9.tar.gz LTS for testing (inactive); — wenzelm / hgweb
#34 (Feb 7, 2021, 12:14:00 AM)
- merge from afp-2021 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- merge from afp-2020 — Gerwin Klein <kleing@unsw.edu.au> / hgweb
- fixed category for Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
- Backed out changeset 4450302adc70 — Manuel Eberl <eberlm@in.tum.de> / hgweb
- fixed category for Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
- sitegen for Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
- New entry: Blue_Eyes — Manuel Eberl <eberlm@in.tum.de> / hgweb
- paragraph tags in the abstract of IsaGeoCoq — paulson <lp15@cam.ac.uk> / hgweb
- tidying of IsaGeoCoq including a shorter abstract and revised title — paulson <lp15@cam.ac.uk> / hgweb
- website for IsaGeoCoq — paulson <lp15@cam.ac.uk> / hgweb
- new entry IsaGeoCoq — paulson <lp15@cam.ac.uk> / hgweb
- hide MB abbreviation — Andreas Lochbihler <mail@andreas-lochbihler.de> / hgweb
- integrate RBT_Impl optimizations — mraszyk / hgweb
#33 (Jan 31, 2021, 12:14:00 AM)
- Simpler proof — nipkow / hgweb
- more robust: support other_isabelle.init_settings for build_history before b93404a4c3dd; — wenzelm / hgweb
- more robust: defer error in sessions structure to build process; — wenzelm / hgweb
- merged, with minor edits: Admin/PLATFORMS, CONTRIBUTORS; — wenzelm / hgweb
- Added tag Isabelle2021-RC3 for changeset 02422c9add5e — wenzelm / hgweb
- provide naproche-20210124 (inactive); — wenzelm / hgweb
- follow stackage update; — wenzelm / hgweb
- tuned name, e.g. relevant for Naproche-SAD debugging in Isabelle/jEdit; — wenzelm / hgweb
- more operations for client connection; — wenzelm / hgweb
- fewer warnings, notably in Naproche-SAD; — wenzelm / hgweb
- suppress bundled Naproche-SAD component: it is in conflict with building the same from sources; — wenzelm / hgweb
- more robust etc/settings; — wenzelm / hgweb
- IDE support for Naproche-SAD; — wenzelm / hgweb
- proper path; — wenzelm / hgweb
- support isabelle components -u and -x; — wenzelm / hgweb
- proper typescript version, required for "vsce package"; — wenzelm / hgweb
- auto-update; — wenzelm / hgweb
- auto-update; — wenzelm / hgweb
- proper type constraint; — wenzelm / hgweb
- VSCode extension for official Isabelle release; — wenzelm / hgweb
- proper message; — wenzelm / hgweb
- unused; — wenzelm / hgweb
- proper heap_free; — wenzelm / hgweb
- suppress markup for literal tokens with block control symbols, for better PIDE/HTML output (see also d15fe10593ff); — wenzelm / hgweb
- clarified documentation concerning macOS Big Sur; — wenzelm / hgweb
- more systematic java-gui-setup, also for "isabelle jedit" command-line tool; — wenzelm / hgweb
- updated to flatlaf-1.0-rc1; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned proofs; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- obsolete; — wenzelm / hgweb
- clarified platforms; — wenzelm / hgweb
- more NEWS; — wenzelm / hgweb
- workaround for Big Sur fullscreen mode: better support for JDialog windows (e.g. Find on top of main View); — wenzelm / hgweb
- clarified app identification, potentially relevant for macOS "defaults"; — wenzelm / hgweb
- updated documentation: HIDPI works smoothly thanks to FlatLaf; — wenzelm / hgweb
- updated for release; — wenzelm / hgweb
- updated screenshot; — wenzelm / hgweb
- clarified reports before errors: support completion of bibtex entries in Isabelle/Scala (amending d01ea9e3bd2d); — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- proper theory_long_name; — wenzelm / hgweb
- updated screenshots; — wenzelm / hgweb
- more robust GUI, notably for Big Sur full-screen where the hypersearch panel becomes a separate maximized window; — wenzelm / hgweb
- revert 1105c42722dc on isabelle-release branch; — wenzelm / hgweb
#33 (Jan 31, 2021, 12:14:00 AM)
- Merge — Simon Foster <simon.foster@york.ac.uk> / hgweb
- Small update to Optics document. — Simon Foster <simon.foster@york.ac.uk> / hgweb
- merged — wenzelm / hgweb
- more generous timeout (25min CPU time); — wenzelm / hgweb
- non-executable files; — wenzelm / hgweb
- Added metadata for previous commit (Optics). — Simon Foster <simon.foster@york.ac.uk> / hgweb
- 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 - adjustments for Word_Lib updates — kleing / hgweb
- sync with l4v — kleing / hgweb
- allow instance for nat
(by Florian) — kleing / hgweb - merge from afp-2020 — kleing / hgweb
- New entry JinjaDCI — nipkow / hgweb
#31 (Jan 17, 2021, 12:14:00 AM)
- back to post-release mode; — wenzelm / hgweb
- Added tag Isabelle2021-RC2 for changeset 802647edfe7b — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- avoid Unicode quotes; — wenzelm / hgweb
- clarified pretty margin: attempt to avoid scrollbar; — wenzelm / hgweb
- more documentation; — wenzelm / hgweb
- more informative errors: simplify diagnosis of spurious failures reported by users; — wenzelm / hgweb